<!DOCTYPE html>
<html class="writer-html5" lang="en" >
<head>
  <meta charset="utf-8" /><meta name="generator" content="Docutils 0.17.1: http://docutils.sourceforge.net/" />

  <meta name="viewport" content="width=device-width, initial-scale=1.0" />
  <title>4. Proofs with structure, II &mdash; The Mechanics of Proof, by Heather Macbeth</title>
      <link rel="stylesheet" href="_static/pygments.css" type="text/css" />
      <link rel="stylesheet" href="_static/css/theme.css" type="text/css" />
      <link rel="stylesheet" href="_static/css/custom.css" type="text/css" />
    <link rel="shortcut icon" href="_static/favicon.ico"/>
  <!--[if lt IE 9]>
    <script src="_static/js/html5shiv.min.js"></script>
  <![endif]-->
  
        <script data-url_root="./" id="documentation_options" src="_static/documentation_options.js"></script>
        <script src="_static/jquery.js"></script>
        <script src="_static/underscore.js"></script>
        <script src="_static/doctools.js"></script>
        <script async="async" src="https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-mml-chtml.js"></script>
    <script src="_static/js/theme.js"></script>
    <link rel="index" title="Index" href="genindex.html" />
    <link rel="search" title="Search" href="search.html" />
    <link rel="next" title="5. Logic" href="05_Logic.html" />
    <link rel="prev" title="3. Parity and divisibility" href="03_Parity_and_Divisibility.html" /> 
</head>

<body class="wy-body-for-nav"> 
  <div class="wy-grid-for-nav">
    <nav data-toggle="wy-nav-shift" class="wy-nav-side">
      <div class="wy-side-scroll">
        <div class="wy-side-nav-search" >
            <a href="index.html" class="icon icon-home"> The Mechanics of Proof
          </a>
<div role="search">
  <form id="rtd-search-form" class="wy-form" action="search.html" method="get">
    <input type="text" name="q" placeholder="Search docs" />
    <input type="hidden" name="check_keywords" value="yes" />
    <input type="hidden" name="area" value="default" />
  </form>
</div>
        </div><div class="wy-menu wy-menu-vertical" data-spy="affix" role="navigation" aria-label="Navigation menu">
              <ul>
<li class="toctree-l1"><a class="reference internal" href="00_Introduction.html">Preface</a></li>
</ul>
<ul class="current">
<li class="toctree-l1"><a class="reference internal" href="01_Proofs_by_Calculation.html">1. Proofs by calculation</a></li>
<li class="toctree-l1"><a class="reference internal" href="02_Proofs_with_Structure.html">2. Proofs with structure</a></li>
<li class="toctree-l1"><a class="reference internal" href="03_Parity_and_Divisibility.html">3. Parity and divisibility</a></li>
<li class="toctree-l1 current"><a class="current reference internal" href="#">4. Proofs with structure, II</a><ul>
<li class="toctree-l2"><a class="reference internal" href="#for-all-and-implication">4.1. &#8220;For all&#8221; and implication</a><ul>
<li class="toctree-l3"><a class="reference internal" href="#example">4.1.1. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#id2">4.1.2. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#id3">4.1.3. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#id4">4.1.4. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#id6">4.1.5. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#id7">4.1.6. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#id8">4.1.7. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#prime-def">4.1.8. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#not-prime">4.1.9. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#exercises">4.1.10. Exercises</a></li>
</ul>
</li>
<li class="toctree-l2"><a class="reference internal" href="#if-and-only-if">4.2. &#8220;If and only if&#8221;</a><ul>
<li class="toctree-l3"><a class="reference internal" href="#id12">4.2.1. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#bezout-iff">4.2.2. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#odd-iff-modeq">4.2.3. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#even-iff-modeq">4.2.4. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#id16">4.2.5. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#id17">4.2.6. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#id18">4.2.7. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#id19">4.2.8. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#even-or-odd-proof">4.2.9. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#id21">4.2.10. Exercises</a></li>
</ul>
</li>
<li class="toctree-l2"><a class="reference internal" href="#there-exists-a-unique">4.3. &#8220;There exists a unique&#8221;</a><ul>
<li class="toctree-l3"><a class="reference internal" href="#id22">4.3.1. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#id23">4.3.2. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#id24">4.3.3. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#division-algorithm">4.3.4. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#id26">4.3.5. Exercises</a></li>
</ul>
</li>
<li class="toctree-l2"><a class="reference internal" href="#contradictory-hypotheses">4.4. Contradictory hypotheses</a><ul>
<li class="toctree-l3"><a class="reference internal" href="#pos-of-mul-pos-right-proof">4.4.1. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#numbers-contradiction">4.4.2. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#mod-contradictory">4.4.3. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#prime-test">4.4.4. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#id31">4.4.5. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#id32">4.4.6. Exercises</a></li>
</ul>
</li>
<li class="toctree-l2"><a class="reference internal" href="#proof-by-contradiction">4.5. Proof by contradiction</a><ul>
<li class="toctree-l3"><a class="reference internal" href="#contradiction-ex1">4.5.1. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#id34">4.5.2. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#id35">4.5.3. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#sq-ne-two">4.5.4. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#even-iff-not-odd">4.5.5. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#id38">4.5.6. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#not-prime-proof">4.5.7. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#not-divisible-proof">4.5.8. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#better-prime-test">4.5.9. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#id42">4.5.10. Exercises</a></li>
</ul>
</li>
</ul>
</li>
<li class="toctree-l1"><a class="reference internal" href="05_Logic.html">5. Logic</a></li>
<li class="toctree-l1"><a class="reference internal" href="06_Induction.html">6. Induction</a></li>
<li class="toctree-l1"><a class="reference internal" href="07_Number_Theory.html">7. Number theory</a></li>
<li class="toctree-l1"><a class="reference internal" href="08_Functions.html">8. Functions</a></li>
<li class="toctree-l1"><a class="reference internal" href="09_Sets.html">9. Sets</a></li>
<li class="toctree-l1"><a class="reference internal" href="10_Relations.html">10. Relations</a></li>
</ul>
<ul>
<li class="toctree-l1"><a class="reference internal" href="Index_of_Tactics.html">Index of Lean tactics</a></li>
<li class="toctree-l1"><a class="reference internal" href="Mainstream_Lean.html">Transitioning to mainstream Lean</a></li>
</ul>

        </div>
      </div>
    </nav>

    <section data-toggle="wy-nav-shift" class="wy-nav-content-wrap"><nav class="wy-nav-top" aria-label="Mobile navigation menu" >
          <i data-toggle="wy-nav-top" class="fa fa-bars"></i>
          <a href="index.html">The Mechanics of Proof</a>
      </nav>

      <div class="wy-nav-content">
        <div class="rst-content">
          <div role="navigation" aria-label="Page navigation">
  <ul class="wy-breadcrumbs">
      <li><a href="index.html" class="icon icon-home"></a> &raquo;</li>
      <li><span class="section-number">4. </span>Proofs with structure, II</li>
      <li class="wy-breadcrumbs-aside">
            <a href="_sources/04_Proofs_with_Structure_II.rst.txt" rel="nofollow"> View page source</a>
      </li>
  </ul>
  <hr/>
</div>
          <div role="main" class="document" itemscope="itemscope" itemtype="http://schema.org/Article">
           <div itemprop="articleBody">
             
  <section id="proofs-with-structure-ii">
<span id="id1"></span><h1><span class="section-number">4. </span>Proofs with structure, II<a class="headerlink" href="#proofs-with-structure-ii" title="Permalink to this headline">&#61633;</a></h1>
<p>In the course of <a class="reference internal" href="02_Proofs_with_Structure.html#proofs-with-structure"><span class="std std-numref">Chapter 2</span></a>, we studied the
logical symbols <span class="math notranslate nohighlight">\(\lor\)</span>, <span class="math notranslate nohighlight">\(\land\)</span> and <span class="math notranslate nohighlight">\(\exists\)</span>, which allow
complicated mathematical statements to be built up from simpler ones.  For each
such symbol, we learned its &#8220;grammar&#8221;: the rule for using it when it appears in a
hypothesis and the rule for using it when it appears in the goal.  This grammar is
called <a class="reference external" href="https://en.wikipedia.org/wiki/Natural_deduction">natural deduction</a>.</p>
<p>This chapter finishes the work started in <a class="reference internal" href="02_Proofs_with_Structure.html#proofs-with-structure"><span class="std std-numref">Chapter 2</span></a>.
We learn the grammar of the remaining logical symbols: <span class="math notranslate nohighlight">\(\forall\)</span>,
<span class="math notranslate nohighlight">\(\to\)</span>, and <span class="math notranslate nohighlight">\(\lnot\)</span>.  We also learn the grammar of two other logical
symbols, <span class="math notranslate nohighlight">\(\leftrightarrow\)</span> and <span class="math notranslate nohighlight">\(\exists!\)</span>, which are less fundamental
because they can be defined in terms of the other ones.</p>
<section id="for-all-and-implication">
<span id="forall-implies"></span><h2><span class="section-number">4.1. </span>&#8220;For all&#8221; and implication<a class="headerlink" href="#for-all-and-implication" title="Permalink to this headline">&#61633;</a></h2>
<section id="example">
<h3><span class="section-number">4.1.1. </span>Example<a class="headerlink" href="#example" title="Permalink to this headline">&#61633;</a></h3>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Let <span class="math notranslate nohighlight">\(a\)</span> be a real number and suppose that for all real numbers <span class="math notranslate nohighlight">\(x\)</span>,
it is true that <span class="math notranslate nohighlight">\(a\le x^2-2x\)</span>.  Show that <span class="math notranslate nohighlight">\(a\le -1\)</span>.</p>
</div>
<figure class="align-center" id="id43">
<a class="reference internal image-reference" href="_images/04_logic_01_parabola.png"><img alt="_images/04_logic_01_parabola.png" src="_images/04_logic_01_parabola.png" style="width: 320.0px; height: 320.0px;" /></a>
<figcaption>
<p><span class="caption-number">Fig. 4.1 </span><span class="caption-text">The parabola <span class="math notranslate nohighlight">\(y= x^2-2x\)</span>.</span><a class="headerlink" href="#id43" title="Permalink to this image">&#61633;</a></p>
</figcaption>
</figure>
<p>Specifying that a formula or predicate is meant to be true for all values of a variable <span class="math notranslate nohighlight">\(x\)</span>,
like we did with <span class="math notranslate nohighlight">\(a\le x^2-2x\)</span> in the above problem, is called <em>universally quantifying</em> over
the variable <span class="math notranslate nohighlight">\(x\)</span>.  It is expressed symbolically as <code class="docutils literal notranslate"><span class="pre">&#8704;</span></code>.</p>
<p>To use a hypothesis with a universal quantifier, you may want to &#8220;specialize&#8221; its use to
one particular variable. For example, in the solution below, we use the special case of the
hypothesis in which <span class="math notranslate nohighlight">\(x\)</span> is set to 1.</p>
<div class="admonition-solution admonition">
<p class="admonition-title">Solution</p>
<div class="math notranslate nohighlight">
\[\begin{split}a &amp;\le  1 ^ 2 - 2 \cdot 1 \\
&amp;= -1.\end{split}\]</div>
</div>
<p>In Lean, perform this specialization using the <code class="docutils literal notranslate"><span class="pre">apply</span></code> tactic.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">{</span><span class="n">a</span> <span class="o">:</span> <span class="n">&#8477;</span><span class="o">}</span> <span class="o">(</span><span class="n">h</span> <span class="o">:</span> <span class="bp">&#8704;</span> <span class="n">x</span><span class="o">,</span> <span class="n">a</span> <span class="bp">&#8804;</span> <span class="n">x</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">-</span> <span class="mi">2</span> <span class="bp">*</span> <span class="n">x</span><span class="o">)</span> <span class="o">:</span> <span class="n">a</span> <span class="bp">&#8804;</span> <span class="bp">-</span><span class="mi">1</span> <span class="o">:=</span>
  <span class="k">calc</span>
    <span class="n">a</span> <span class="bp">&#8804;</span> <span class="mi">1</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">-</span> <span class="mi">2</span> <span class="bp">*</span> <span class="mi">1</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">apply</span> <span class="n">h</span>
    <span class="n">_</span> <span class="bp">=</span> <span class="bp">-</span><span class="mi">1</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">numbers</span>
</pre></div>
</div>
</section>
<section id="id2">
<h3><span class="section-number">4.1.2. </span>Example<a class="headerlink" href="#id2" title="Permalink to this headline">&#61633;</a></h3>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Let <span class="math notranslate nohighlight">\(n\)</span> be a natural number which is a factor of every natural number <span class="math notranslate nohighlight">\(m\)</span>.  Show that
<span class="math notranslate nohighlight">\(n=1\)</span>.</p>
</div>
<div class="admonition-solution admonition">
<p class="admonition-title">Solution</p>
<p>Since <span class="math notranslate nohighlight">\(n\)</span> is a factor of every natural number, it is a factor of <span class="math notranslate nohighlight">\(1\)</span>.  Also notice
that <span class="math notranslate nohighlight">\(1\)</span> is positive. So we can invoke the size bounds on factors discussed in
<a class="reference internal" href="03_Parity_and_Divisibility.html#dvd-bd-1"><span class="std std-numref">Example 3.2.7</span></a> and <a class="reference internal" href="03_Parity_and_Divisibility.html#dvd-bd-2"><span class="std std-numref">Example 3.2.8</span></a>: <span class="math notranslate nohighlight">\(n\le 1\)</span> and
<span class="math notranslate nohighlight">\(1 \le n\)</span>.  Therefore <span class="math notranslate nohighlight">\(n=1\)</span>.</p>
</div>
<p>For the Lean proof, we recall that the bound from <a class="reference internal" href="03_Parity_and_Divisibility.html#dvd-bd-1"><span class="std std-numref">Example 3.2.7</span></a> is in Lean as
<code class="docutils literal notranslate"><span class="pre">Nat.le_of_dvd</span></code>, and the bound from <a class="reference internal" href="03_Parity_and_Divisibility.html#dvd-bd-2"><span class="std std-numref">Example 3.2.8</span></a> is in Lean as
<code class="docutils literal notranslate"><span class="pre">Nat.pos_of_dvd_of_pos</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">{</span><span class="n">n</span> <span class="o">:</span> <span class="n">&#8469;</span><span class="o">}</span> <span class="o">(</span><span class="n">hn</span> <span class="o">:</span> <span class="bp">&#8704;</span> <span class="n">m</span><span class="o">,</span> <span class="n">n</span> <span class="bp">&#8739;</span> <span class="n">m</span><span class="o">)</span> <span class="o">:</span> <span class="n">n</span> <span class="bp">=</span> <span class="mi">1</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="k">have</span> <span class="n">h1</span> <span class="o">:</span> <span class="n">n</span> <span class="bp">&#8739;</span> <span class="mi">1</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">apply</span> <span class="n">hn</span>
  <span class="k">have</span> <span class="n">h2</span> <span class="o">:</span> <span class="mi">0</span> <span class="bp">&lt;</span> <span class="mi">1</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">numbers</span>
  <span class="n">apply</span> <span class="n">le_antisymm</span>
  <span class="bp">&#183;</span> <span class="n">apply</span> <span class="n">Nat.le_of_dvd</span> <span class="n">h2</span> <span class="n">h1</span>
  <span class="bp">&#183;</span> <span class="n">apply</span> <span class="n">Nat.pos_of_dvd_of_pos</span> <span class="n">h1</span> <span class="n">h2</span>
</pre></div>
</div>
</section>
<section id="id3">
<h3><span class="section-number">4.1.3. </span>Example<a class="headerlink" href="#id3" title="Permalink to this headline">&#61633;</a></h3>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Let <span class="math notranslate nohighlight">\(a\)</span> and <span class="math notranslate nohighlight">\(b\)</span> be real numbers and suppose that every real number <span class="math notranslate nohighlight">\(x\)</span> is
either at least <span class="math notranslate nohighlight">\(a\)</span> or at most <span class="math notranslate nohighlight">\(b\)</span>. Show that <span class="math notranslate nohighlight">\(a \le b\)</span>.</p>
</div>
<div class="admonition-solution admonition">
<p class="admonition-title">Solution</p>
<p>Consider the real number <span class="math notranslate nohighlight">\(\frac {a+b}{2}\)</span>.  It is either at least <span class="math notranslate nohighlight">\(a\)</span> or at most
<span class="math notranslate nohighlight">\(b\)</span>.</p>
<p><strong>Case 1:</strong> <span class="math notranslate nohighlight">\(\frac {a+b}{2} \geq a\)</span>. Then</p>
<div class="math notranslate nohighlight">
\[\begin{split}b &amp;= 2 \left(\frac{a + b} {2}\right) - a\\
&amp;\geq 2 \cdot a - a \\
&amp; = a.\end{split}\]</div>
<p><strong>Case 2:</strong> <span class="math notranslate nohighlight">\(\frac {a+b}{2} \leq b\)</span>.  Then</p>
<div class="math notranslate nohighlight">
\[\begin{split}a &amp;= 2 \left(\frac{a + b} {2}\right) - b\\
&amp;\leq 2 \cdot b - b \\
&amp; = b.\end{split}\]</div>
</div>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">{</span><span class="n">a</span> <span class="n">b</span> <span class="o">:</span> <span class="n">&#8477;</span><span class="o">}</span> <span class="o">(</span><span class="n">h</span> <span class="o">:</span> <span class="bp">&#8704;</span> <span class="n">x</span><span class="o">,</span> <span class="n">x</span> <span class="bp">&#8805;</span> <span class="n">a</span> <span class="bp">&#8744;</span> <span class="n">x</span> <span class="bp">&#8804;</span> <span class="n">b</span><span class="o">)</span> <span class="o">:</span> <span class="n">a</span> <span class="bp">&#8804;</span> <span class="n">b</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</section>
<section id="id4">
<h3><span class="section-number">4.1.4. </span>Example<a class="headerlink" href="#id4" title="Permalink to this headline">&#61633;</a></h3>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Let <span class="math notranslate nohighlight">\(a\)</span> be real number whose square is at most 2, and which is greater than or equal to
any real number whose square is at most 2. <a class="footnote-reference brackets" href="#id11" id="id5">1</a> Let <span class="math notranslate nohighlight">\(b\)</span> be another real number with the same
two properties.  Prove that <span class="math notranslate nohighlight">\(a=b\)</span>.</p>
</div>
<p>Consider the hypothesis in this problem that</p>
<blockquote>
<div><p><span class="math notranslate nohighlight">\(a\)</span> is greater than or equal to any real number whose square is at most 2.</p>
</div></blockquote>
<p>Implicitly, there is a universal quantification (&#8220;any real number&#8221;), and also an <em>implication</em>,
so a more pedantic version of this hypothesis would be</p>
<blockquote>
<div><p>for all real numbers <span class="math notranslate nohighlight">\(y\)</span>, if <span class="math notranslate nohighlight">\(y^2\le 2\)</span> then <span class="math notranslate nohighlight">\(y\le a\)</span>.</p>
</div></blockquote>
<p>We can specialize such a hypothesis to any particular choice of <span class="math notranslate nohighlight">\(y\)</span> for which the
<em>antecedent</em> <span class="math notranslate nohighlight">\(y^2\le 2\)</span> is true.</p>
<div class="admonition-solution admonition">
<p class="admonition-title">Solution</p>
<p>Since <span class="math notranslate nohighlight">\(a^2\le 2\)</span>, and <span class="math notranslate nohighlight">\(b\)</span> is greater than or equal to any real number whose square is
at most 2, <span class="math notranslate nohighlight">\(a \le b\)</span>.</p>
<p>Since <span class="math notranslate nohighlight">\(b^2\le 2\)</span>, and <span class="math notranslate nohighlight">\(a\)</span> is greater than or equal to any real number whose square is
at most 2, <span class="math notranslate nohighlight">\(b \le a\)</span>.</p>
<p>Therefore <span class="math notranslate nohighlight">\(a=b\)</span>.</p>
</div>
<p>In Lean, an implication is expressed using the symbol <code class="docutils literal notranslate"><span class="pre">&#8594;</span></code>.  The tactic <code class="docutils literal notranslate"><span class="pre">apply</span></code> works for
hypotheses featuring implications.  In the proof below, the goal state before <code class="docutils literal notranslate"><span class="pre">apply</span> <span class="pre">hb2</span></code> is</p>
<div class="highlight-text notranslate"><div class="highlight"><pre><span></span>a b: &#8477;
ha1 : a ^ 2 &#8804; 2
hb1 : b ^ 2 &#8804; 2
ha2 : &#8704; (y : &#8477;), y ^ 2 &#8804; 2 &#8594; y &#8804; a
hb2 : &#8704; (y : &#8477;), y ^ 2 &#8804; 2 &#8594; y &#8804; b
&#8866; a &#8804; b
</pre></div>
</div>
<p>and the goal state after it is</p>
<div class="highlight-text notranslate"><div class="highlight"><pre><span></span>a b : &#8477;
ha1 : a ^ 2 &#8804; 2
hb1 : b ^ 2 &#8804; 2
ha2 : &#8704; (y : &#8477;), y ^ 2 &#8804; 2 &#8594; y &#8804; a
hb2 : &#8704; (y : &#8477;), y ^ 2 &#8804; 2 &#8594; y &#8804; b
&#8866; a ^ 2 &#8804; 2
</pre></div>
</div>
<p>The hypothesis <code class="docutils literal notranslate"><span class="pre">&#8704;</span> <span class="pre">(y</span> <span class="pre">:</span> <span class="pre">&#8477;),</span> <span class="pre">y</span> <span class="pre">^</span> <span class="pre">2</span> <span class="pre">&#8804;</span> <span class="pre">2</span> <span class="pre">&#8594;</span> <span class="pre">y</span> <span class="pre">&#8804;</span> <span class="pre">b</span></code> has been applied to the goal <code class="docutils literal notranslate"><span class="pre">a</span> <span class="pre">&#8804;</span> <span class="pre">b</span></code>, leaving
the hopefully-easier goal <code class="docutils literal notranslate"><span class="pre">a</span> <span class="pre">^</span> <span class="pre">2</span> <span class="pre">&#8804;</span> <span class="pre">2</span></code>: proving the antecedent of the implication.</p>
<p>Fill in the second part of the proof.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">{</span><span class="n">a</span> <span class="n">b</span> <span class="o">:</span> <span class="n">&#8477;</span><span class="o">}</span> <span class="o">(</span><span class="n">ha1</span> <span class="o">:</span> <span class="n">a</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">&#8804;</span> <span class="mi">2</span><span class="o">)</span> <span class="o">(</span><span class="n">hb1</span> <span class="o">:</span> <span class="n">b</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">&#8804;</span> <span class="mi">2</span><span class="o">)</span> <span class="o">(</span><span class="n">ha2</span> <span class="o">:</span> <span class="bp">&#8704;</span> <span class="n">y</span><span class="o">,</span> <span class="n">y</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">&#8804;</span> <span class="mi">2</span> <span class="bp">&#8594;</span> <span class="n">y</span> <span class="bp">&#8804;</span> <span class="n">a</span><span class="o">)</span>
    <span class="o">(</span><span class="n">hb2</span> <span class="o">:</span> <span class="bp">&#8704;</span> <span class="n">y</span><span class="o">,</span> <span class="n">y</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">&#8804;</span> <span class="mi">2</span> <span class="bp">&#8594;</span> <span class="n">y</span> <span class="bp">&#8804;</span> <span class="n">b</span><span class="o">)</span> <span class="o">:</span>
    <span class="n">a</span> <span class="bp">=</span> <span class="n">b</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">apply</span> <span class="n">le_antisymm</span>
  <span class="bp">&#183;</span> <span class="n">apply</span> <span class="n">hb2</span>
    <span class="n">apply</span> <span class="n">ha1</span>
  <span class="bp">&#183;</span> <span class="gr">sorry</span>
</pre></div>
</div>
</section>
<section id="id6">
<h3><span class="section-number">4.1.5. </span>Example<a class="headerlink" href="#id6" title="Permalink to this headline">&#61633;</a></h3>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Show that there exists a real number <span class="math notranslate nohighlight">\(b\)</span> such that for every real number <span class="math notranslate nohighlight">\(x\)</span>,
it is true that <span class="math notranslate nohighlight">\(b \le x^2-2x\)</span>.</p>
</div>
<p>Notice that in this problem a universally quantified statement appears in the goal:
&#8220;for every real number <span class="math notranslate nohighlight">\(x\)</span>, &#8230;.&#8221;</p>
<div class="admonition-solution admonition">
<p class="admonition-title">Solution</p>
<p>We show that -1 has this property.  Indeed, let <span class="math notranslate nohighlight">\(x\)</span> be a real number; then</p>
<div class="math notranslate nohighlight">
\[\begin{split}-1 &amp;\le -1 + (x-1)^2 \\
&amp;=x^2-2x.\end{split}\]</div>
</div>
<p>We solve the problem by formally introducing a particular, arbitrary real number <span class="math notranslate nohighlight">\(x\)</span> (&#8220;let
<span class="math notranslate nohighlight">\(x\)</span> be a real number&#8221;) and proving the desired statement for that <span class="math notranslate nohighlight">\(x\)</span>.  In Lean this
argument is performed by the tactic <code class="docutils literal notranslate"><span class="pre">intro</span></code>.  Before the use of this tactic, the goal state is</p>
<div class="highlight-text notranslate"><div class="highlight"><pre><span></span>&#8866; &#8704; (x : &#8477;), -1 &#8804; x ^ 2 - 2 * x
</pre></div>
</div>
<p>After the use of this tactic, the goal state is</p>
<div class="highlight-text notranslate"><div class="highlight"><pre><span></span>x : &#8477;
&#8866; -1 &#8804; x ^ 2 - 2 * x
</pre></div>
</div>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="bp">&#8707;</span> <span class="n">b</span> <span class="o">:</span> <span class="n">&#8477;</span><span class="o">,</span> <span class="bp">&#8704;</span> <span class="n">x</span> <span class="o">:</span> <span class="n">&#8477;</span><span class="o">,</span> <span class="n">b</span> <span class="bp">&#8804;</span> <span class="n">x</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">-</span> <span class="mi">2</span> <span class="bp">*</span> <span class="n">x</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">use</span> <span class="bp">-</span><span class="mi">1</span>
  <span class="n">intro</span> <span class="n">x</span>
  <span class="k">calc</span>
    <span class="bp">-</span><span class="mi">1</span> <span class="bp">&#8804;</span> <span class="bp">-</span><span class="mi">1</span> <span class="bp">+</span> <span class="o">(</span><span class="n">x</span> <span class="bp">-</span> <span class="mi">1</span><span class="o">)</span> <span class="bp">^</span> <span class="mi">2</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">extra</span>
    <span class="n">_</span> <span class="bp">=</span> <span class="n">x</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">-</span> <span class="mi">2</span> <span class="bp">*</span> <span class="n">x</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">ring</span>
</pre></div>
</div>
</section>
<section id="id7">
<h3><span class="section-number">4.1.6. </span>Example<a class="headerlink" href="#id7" title="Permalink to this headline">&#61633;</a></h3>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Show that there exists a real number <span class="math notranslate nohighlight">\(c\)</span> such that for all real numbers <span class="math notranslate nohighlight">\(x\)</span> and
<span class="math notranslate nohighlight">\(y\)</span>, if <span class="math notranslate nohighlight">\(x^2+y^2\le 4\)</span>, then <span class="math notranslate nohighlight">\(x+y\geq c\)</span>.</p>
</div>
<p>Here the goal contains universal quantification over <span class="math notranslate nohighlight">\(x\)</span> and <span class="math notranslate nohighlight">\(y\)</span>, as well as an
implication: &#8220;if <span class="math notranslate nohighlight">\(x^2+y^2\le 4\)</span>, then &#8230;.&#8221;  In solving the problem, we formally introduce
the variables <span class="math notranslate nohighlight">\(x\)</span> and <span class="math notranslate nohighlight">\(y\)</span> and also the hypothesis <span class="math notranslate nohighlight">\(x^2+y^2\le 4\)</span> which they are
assumed to satisfy:</p>
<div class="admonition-solution admonition">
<p class="admonition-title">Solution</p>
<p>We show that -3 has this property.  Indeed, let <span class="math notranslate nohighlight">\(x\)</span> and <span class="math notranslate nohighlight">\(y\)</span> be real numbers and
suppose that <span class="math notranslate nohighlight">\(x^2+y^2\le 4\)</span>.  Then</p>
<div class="math notranslate nohighlight">
\[\begin{split}(x + y) ^ 2 &amp;\le (x + y) ^ 2 + (x - y) ^ 2 \\
&amp;= 2 (x ^ 2 + y ^ 2) \\
&amp;\le 2 \cdot 4 \\
&amp;\le 3 ^ 2.\end{split}\]</div>
<p>So <span class="math notranslate nohighlight">\(x + y \geq -3\)</span> (and also <span class="math notranslate nohighlight">\(x + y \leq 3\)</span>).</p>
</div>
<p>In Lean, the introduction of both the variables <span class="math notranslate nohighlight">\(x\)</span> and <span class="math notranslate nohighlight">\(y\)</span> and the hypothesis
<span class="math notranslate nohighlight">\(x^2+y^2\le 4\)</span> is done using the <code class="docutils literal notranslate"><span class="pre">intro</span></code> tactic.  To deduce from
<span class="math notranslate nohighlight">\((x + y) ^ 2 \le 3 ^ 2\)</span> that <span class="math notranslate nohighlight">\(-3 &#8804; x + y\)</span> and <span class="math notranslate nohighlight">\(x + y &#8804; 3\)</span>, you will need to use
the lemma</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">lemma</span> <span class="n">abs_le_of_sq_le_sq&#39;</span> <span class="o">(</span><span class="n">h</span> <span class="o">:</span> <span class="n">x</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">&#8804;</span> <span class="n">y</span> <span class="bp">^</span> <span class="mi">2</span><span class="o">)</span> <span class="o">(</span><span class="n">hy</span> <span class="o">:</span> <span class="mi">0</span> <span class="bp">&#8804;</span> <span class="n">y</span><span class="o">)</span> <span class="o">:</span> <span class="bp">-</span><span class="n">y</span> <span class="bp">&#8804;</span> <span class="n">x</span> <span class="bp">&#8743;</span> <span class="n">x</span> <span class="bp">&#8804;</span> <span class="n">y</span> <span class="o">:=</span>
</pre></div>
</div>
<p>which we previously saw in <a class="reference internal" href="02_Proofs_with_Structure.html#abs-le-of-sq-le-sq"><span class="std std-numref">Example 2.4.2</span></a>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="bp">&#8707;</span> <span class="n">c</span> <span class="o">:</span> <span class="n">&#8477;</span><span class="o">,</span> <span class="bp">&#8704;</span> <span class="n">x</span> <span class="n">y</span><span class="o">,</span> <span class="n">x</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">+</span> <span class="n">y</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">&#8804;</span> <span class="mi">4</span> <span class="bp">&#8594;</span> <span class="n">x</span> <span class="bp">+</span> <span class="n">y</span> <span class="bp">&#8805;</span> <span class="n">c</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</section>
<section id="id8">
<h3><span class="section-number">4.1.7. </span>Example<a class="headerlink" href="#id8" title="Permalink to this headline">&#61633;</a></h3>
<div class="admonition-definition admonition">
<p class="admonition-title">Definition</p>
<p>A property is true <em>for all sufficiently large integers</em> <span class="math notranslate nohighlight">\(n\)</span>, if there exists an integer
<span class="math notranslate nohighlight">\(N\)</span>, such that that property is true for all integers <span class="math notranslate nohighlight">\(n\geq N\)</span>.</p>
</div>
<p>Likewise for rational numbers, real numbers, &#8230;.</p>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Show that for all sufficiently large integers <span class="math notranslate nohighlight">\(n\)</span>, it is true that
<span class="math notranslate nohighlight">\(n ^ 3 &#8805; 4n ^ 2 + 7\)</span>.</p>
</div>
<p>In the solution that follows, &#8220;For all <span class="math notranslate nohighlight">\(n\geq 5\)</span>&#8221; is a shorter way of expressing, &#8220;Let
<span class="math notranslate nohighlight">\(n\)</span> be an integer and suppose that <span class="math notranslate nohighlight">\(n\geq 5\)</span>&#8221;.</p>
<div class="admonition-solution admonition">
<p class="admonition-title">Solution</p>
<p>For all <span class="math notranslate nohighlight">\(n\geq 5\)</span>,</p>
<div class="math notranslate nohighlight">
\[\begin{split}n ^ 3 &amp;= n \cdot n ^ 2 \\
&amp;\geq 5 n ^ 2 \\
&amp; = 4 n ^ 2 + n ^ 2\\
&amp; \geq 4 n ^ 2 + 5 ^ 2 \\
&amp; = 4 n ^ 2 + 7 + 18 \\
&amp; &#8805; 4 n ^ 2 + 7.\end{split}\]</div>
</div>
<p>I have provided the notation <code class="docutils literal notranslate"><span class="pre">forall_sufficiently_large</span></code> to express this and similar problems in
Lean.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="n">forall_sufficiently_large</span> <span class="n">n</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">,</span> <span class="n">n</span> <span class="bp">^</span> <span class="mi">3</span> <span class="bp">&#8805;</span> <span class="mi">4</span> <span class="bp">*</span> <span class="n">n</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">+</span> <span class="mi">7</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">dsimp</span>
  <span class="n">use</span> <span class="mi">5</span>
  <span class="n">intro</span> <span class="n">n</span> <span class="n">hn</span>
  <span class="k">calc</span>
    <span class="n">n</span> <span class="bp">^</span> <span class="mi">3</span> <span class="bp">=</span> <span class="n">n</span> <span class="bp">*</span> <span class="n">n</span> <span class="bp">^</span> <span class="mi">2</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">ring</span>
    <span class="n">_</span> <span class="bp">&#8805;</span> <span class="mi">5</span> <span class="bp">*</span> <span class="n">n</span> <span class="bp">^</span> <span class="mi">2</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">rel</span> <span class="o">[</span><span class="n">hn</span><span class="o">]</span>
    <span class="n">_</span> <span class="bp">=</span> <span class="mi">4</span> <span class="bp">*</span> <span class="n">n</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">+</span> <span class="n">n</span> <span class="bp">^</span> <span class="mi">2</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">ring</span>
    <span class="n">_</span> <span class="bp">&#8805;</span> <span class="mi">4</span> <span class="bp">*</span> <span class="n">n</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">+</span> <span class="mi">5</span> <span class="bp">^</span> <span class="mi">2</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">rel</span> <span class="o">[</span><span class="n">hn</span><span class="o">]</span>
    <span class="n">_</span> <span class="bp">=</span> <span class="mi">4</span> <span class="bp">*</span> <span class="n">n</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">+</span> <span class="mi">7</span> <span class="bp">+</span> <span class="mi">18</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">ring</span>
    <span class="n">_</span> <span class="bp">&#8805;</span> <span class="mi">4</span> <span class="bp">*</span> <span class="n">n</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">+</span> <span class="mi">7</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">extra</span>
</pre></div>
</div>
</section>
<section id="prime-def">
<span id="id9"></span><h3><span class="section-number">4.1.8. </span>Example<a class="headerlink" href="#prime-def" title="Permalink to this headline">&#61633;</a></h3>
<div class="admonition-definition admonition">
<p class="admonition-title">Definition</p>
<p>A natural number <span class="math notranslate nohighlight">\(p\)</span> is <em>prime</em>, if it is at least <span class="math notranslate nohighlight">\(2\)</span>, and the only factors
of <span class="math notranslate nohighlight">\(p\)</span> are <span class="math notranslate nohighlight">\(1\)</span> and <span class="math notranslate nohighlight">\(p\)</span>.</p>
</div>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">def</span> <span class="n">Prime</span> <span class="o">(</span><span class="n">p</span> <span class="o">:</span> <span class="n">&#8469;</span><span class="o">)</span> <span class="o">:</span> <span class="kt">Prop</span> <span class="o">:=</span>
  <span class="mi">2</span> <span class="bp">&#8804;</span> <span class="n">p</span> <span class="bp">&#8743;</span> <span class="bp">&#8704;</span> <span class="n">m</span> <span class="o">:</span> <span class="n">&#8469;</span><span class="o">,</span> <span class="n">m</span> <span class="bp">&#8739;</span> <span class="n">p</span> <span class="bp">&#8594;</span> <span class="n">m</span> <span class="bp">=</span> <span class="mi">1</span> <span class="bp">&#8744;</span> <span class="n">m</span> <span class="bp">=</span> <span class="n">p</span>
</pre></div>
</div>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Show that 2 is prime.</p>
</div>
<div class="admonition-solution admonition">
<p class="admonition-title">Solution</p>
<p>Clearly <span class="math notranslate nohighlight">\(2 \le 2\)</span>.  Let <span class="math notranslate nohighlight">\(m\)</span> be a factor of <span class="math notranslate nohighlight">\(2\)</span>.  Since <span class="math notranslate nohighlight">\(2\)</span> is positive,
by the size bounds on factors discussed in <a class="reference internal" href="03_Parity_and_Divisibility.html#dvd-bd-1"><span class="std std-numref">Example 3.2.7</span></a> and
<a class="reference internal" href="03_Parity_and_Divisibility.html#dvd-bd-2"><span class="std std-numref">Example 3.2.8</span></a>, we have that <span class="math notranslate nohighlight">\(m \le 2\)</span> and <span class="math notranslate nohighlight">\(1 \le m\)</span>.  The only
natural numbers <span class="math notranslate nohighlight">\(m\)</span> satisfying <span class="math notranslate nohighlight">\(m \le 2\)</span> and <span class="math notranslate nohighlight">\(1 \le m\)</span> are <span class="math notranslate nohighlight">\(1\)</span> and
<span class="math notranslate nohighlight">\(2\)</span>, so as required <span class="math notranslate nohighlight">\(m=1\)</span> or <span class="math notranslate nohighlight">\(m=2\)</span>.</p>
</div>
<p>One new technique used in this solution is to observe from numeric bounds on a natural number (like
<span class="math notranslate nohighlight">\(m \le 2\)</span> and <span class="math notranslate nohighlight">\(1 \le m\)</span> here) that there are finitely many possibilities (here,
<span class="math notranslate nohighlight">\(m=1\)</span> or <span class="math notranslate nohighlight">\(m=2\)</span>.)  In Lean, we use the tactic <code class="docutils literal notranslate"><span class="pre">interval_cases</span></code> for this kind of
argument.  It also works for integers, but it doesn&#8217;t work for rational numbers or real numbers &#8211;
why?</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="n">Prime</span> <span class="mi">2</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">constructor</span>
  <span class="bp">&#183;</span> <span class="n">numbers</span> <span class="c1">-- show `2 &#8804; 2`</span>
  <span class="n">intro</span> <span class="n">m</span> <span class="n">hmp</span>
  <span class="k">have</span> <span class="n">hp</span> <span class="o">:</span> <span class="mi">0</span> <span class="bp">&lt;</span> <span class="mi">2</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">numbers</span>
  <span class="k">have</span> <span class="n">hmp_le</span> <span class="o">:</span> <span class="n">m</span> <span class="bp">&#8804;</span> <span class="mi">2</span> <span class="o">:=</span> <span class="n">Nat.le_of_dvd</span> <span class="n">hp</span> <span class="n">hmp</span>
  <span class="k">have</span> <span class="n">h1m</span> <span class="o">:</span> <span class="mi">1</span> <span class="bp">&#8804;</span> <span class="n">m</span> <span class="o">:=</span> <span class="n">Nat.pos_of_dvd_of_pos</span> <span class="n">hmp</span> <span class="n">hp</span>
  <span class="n">interval_cases</span> <span class="n">m</span>
  <span class="bp">&#183;</span> <span class="n">left</span>
    <span class="n">numbers</span> <span class="c1">-- show `1 = 1`</span>
  <span class="bp">&#183;</span> <span class="n">right</span>
    <span class="n">numbers</span> <span class="c1">-- show `2 = 2`</span>
</pre></div>
</div>
<p>This lemma is available for future use in Lean under the name <code class="docutils literal notranslate"><span class="pre">prime_two</span></code>.</p>
</section>
<section id="not-prime">
<span id="id10"></span><h3><span class="section-number">4.1.9. </span>Example<a class="headerlink" href="#not-prime" title="Permalink to this headline">&#61633;</a></h3>
<p>You might be wondering how to prove that a natural number <span class="math notranslate nohighlight">\(p\)</span> is <em>not</em> prime.  The idea is to
show that it can be expressed as a nontrivial product.</p>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Show that 6 is not prime.</p>
</div>
<div class="admonition-solution admonition">
<p class="admonition-title">Solution</p>
<p><span class="math notranslate nohighlight">\(6=2\cdot 3\)</span>, so <span class="math notranslate nohighlight">\(2 \mid 6\)</span>.  But <span class="math notranslate nohighlight">\(2 \ne 1\)</span> and <span class="math notranslate nohighlight">\(2 \ne 6\)</span>.</p>
</div>
<p>We will prove this test carefully in <a class="reference internal" href="#not-prime-proof"><span class="std std-numref">Example 4.5.7</span></a>.  For now, feel free to
use it.  In Lean the lemma name is <code class="docutils literal notranslate"><span class="pre">not_prime</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="bp">&#172;</span> <span class="n">Prime</span> <span class="mi">6</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">apply</span> <span class="n">not_prime</span> <span class="mi">2</span> <span class="mi">3</span>
  <span class="bp">&#183;</span> <span class="n">numbers</span> <span class="c1">-- show `2 &#8800; 1`</span>
  <span class="bp">&#183;</span> <span class="n">numbers</span> <span class="c1">-- show `2 &#8800; 6`</span>
  <span class="bp">&#183;</span> <span class="n">numbers</span> <span class="c1">-- show `6 = 2 * 3`</span>
</pre></div>
</div>
</section>
<section id="exercises">
<h3><span class="section-number">4.1.10. </span>Exercises<a class="headerlink" href="#exercises" title="Permalink to this headline">&#61633;</a></h3>
<ol class="arabic">
<li><p>Let <span class="math notranslate nohighlight">\(a\)</span> be a rational number and suppose that for all rational numbers <span class="math notranslate nohighlight">\(b\)</span>,
<span class="math notranslate nohighlight">\(a\ge -3+4b-b^2\)</span>.  Show that <span class="math notranslate nohighlight">\(a\ge 1\)</span>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">{</span><span class="n">a</span> <span class="o">:</span> <span class="n">&#8474;</span><span class="o">}</span> <span class="o">(</span><span class="n">h</span> <span class="o">:</span> <span class="bp">&#8704;</span> <span class="n">b</span> <span class="o">:</span> <span class="n">&#8474;</span><span class="o">,</span> <span class="n">a</span> <span class="bp">&#8805;</span> <span class="bp">-</span><span class="mi">3</span> <span class="bp">+</span> <span class="mi">4</span> <span class="bp">*</span> <span class="n">b</span> <span class="bp">-</span> <span class="n">b</span> <span class="bp">^</span> <span class="mi">2</span><span class="o">)</span> <span class="o">:</span> <span class="n">a</span> <span class="bp">&#8805;</span> <span class="mi">1</span> <span class="o">:=</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Let <span class="math notranslate nohighlight">\(n\)</span> be an integer and suppose that every integer <span class="math notranslate nohighlight">\(m\)</span> between 1 and 5 is a
factor of <span class="math notranslate nohighlight">\(n\)</span>. Show that 15 is a factor of <span class="math notranslate nohighlight">\(n\)</span>.  (You may need to review
<a class="reference internal" href="03_Parity_and_Divisibility.html#bezout"><span class="std std-numref">Section 3.5</span></a>.)</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">{</span><span class="n">n</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">}</span> <span class="o">(</span><span class="n">hn</span> <span class="o">:</span> <span class="bp">&#8704;</span> <span class="n">m</span><span class="o">,</span> <span class="mi">1</span> <span class="bp">&#8804;</span> <span class="n">m</span> <span class="bp">&#8594;</span> <span class="n">m</span> <span class="bp">&#8804;</span> <span class="mi">5</span> <span class="bp">&#8594;</span> <span class="n">m</span> <span class="bp">&#8739;</span> <span class="n">n</span><span class="o">)</span> <span class="o">:</span> <span class="mi">15</span> <span class="bp">&#8739;</span> <span class="n">n</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Show that there exists a natural number <span class="math notranslate nohighlight">\(n\)</span> such that every natural number <span class="math notranslate nohighlight">\(m\)</span> is at
least <span class="math notranslate nohighlight">\(n\)</span>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="bp">&#8707;</span> <span class="n">n</span> <span class="o">:</span> <span class="n">&#8469;</span><span class="o">,</span> <span class="bp">&#8704;</span> <span class="n">m</span> <span class="o">:</span> <span class="n">&#8469;</span><span class="o">,</span> <span class="n">n</span> <span class="bp">&#8804;</span> <span class="n">m</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Show that there exists a real number <span class="math notranslate nohighlight">\(a\)</span>, such that for all real numbers <span class="math notranslate nohighlight">\(b\)</span>, there
exists a real number <span class="math notranslate nohighlight">\(c\)</span>, such that <span class="math notranslate nohighlight">\(a + b &lt; c\)</span>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="bp">&#8707;</span> <span class="n">a</span> <span class="o">:</span> <span class="n">&#8477;</span><span class="o">,</span> <span class="bp">&#8704;</span> <span class="n">b</span> <span class="o">:</span> <span class="n">&#8477;</span><span class="o">,</span> <span class="bp">&#8707;</span> <span class="n">c</span> <span class="o">:</span> <span class="n">&#8477;</span><span class="o">,</span> <span class="n">a</span> <span class="bp">+</span> <span class="n">b</span> <span class="bp">&lt;</span> <span class="n">c</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Show that for all sufficiently large real numbers <span class="math notranslate nohighlight">\(x\)</span>,
<span class="math notranslate nohighlight">\(x ^ 3 + 3 x &#8805; 7 x ^ 2 + 12\)</span>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="n">forall_sufficiently_large</span> <span class="n">x</span> <span class="o">:</span> <span class="n">&#8477;</span><span class="o">,</span> <span class="n">x</span> <span class="bp">^</span> <span class="mi">3</span> <span class="bp">+</span> <span class="mi">3</span> <span class="bp">*</span> <span class="n">x</span> <span class="bp">&#8805;</span> <span class="mi">7</span> <span class="bp">*</span> <span class="n">x</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">+</span> <span class="mi">12</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Show that 45 is not prime.</p>
<p>You may use the Lean lemma <code class="docutils literal notranslate"><span class="pre">not_prime</span></code>, as in <a class="reference internal" href="#not-prime"><span class="std std-numref">Example 4.1.9</span></a>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="bp">&#172;</span><span class="o">(</span><span class="n">Prime</span> <span class="mi">45</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
</ol>
<p class="rubric">Footnotes</p>
<dl class="footnote brackets">
<dt class="label" id="id11"><span class="brackets"><a class="fn-backref" href="#id5">1</a></span></dt>
<dd><p>That is, <span class="math notranslate nohighlight">\(a\)</span> is <em>maximal in the set of real numbers whose square is at most 2.</em></p>
</dd>
</dl>
</section>
</section>
<section id="if-and-only-if">
<span id="iff"></span><h2><span class="section-number">4.2. </span>&#8220;If and only if&#8221;<a class="headerlink" href="#if-and-only-if" title="Permalink to this headline">&#61633;</a></h2>
<section id="id12">
<h3><span class="section-number">4.2.1. </span>Example<a class="headerlink" href="#id12" title="Permalink to this headline">&#61633;</a></h3>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Let <span class="math notranslate nohighlight">\(a\)</span> be a rational number.  Show that <span class="math notranslate nohighlight">\(3a+1\le 7\)</span> if and only if <span class="math notranslate nohighlight">\(a\le 2\)</span>.</p>
</div>
<p>The phrase &#8220;if and only if&#8221; means exactly what it sounds like.  In this problem we have to show
(1) if <span class="math notranslate nohighlight">\(3a+1\le 7\)</span> then <span class="math notranslate nohighlight">\(a\le 2\)</span> and (2) if <span class="math notranslate nohighlight">\(a\le 2\)</span> then <span class="math notranslate nohighlight">\(3a+1\le 7\)</span>.</p>
<div class="admonition-solution admonition">
<p class="admonition-title">Solution</p>
<p>First, suppose that <span class="math notranslate nohighlight">\(3a+1\le 7\)</span>. Then</p>
<div class="math notranslate nohighlight">
\[\begin{split}a&amp;=\frac{(3a+1)-1}{3}\\
&amp;\le \frac{7-1}{3}\\
&amp;=2.\end{split}\]</div>
<p>Conversely, suppose that <span class="math notranslate nohighlight">\(a\le 2\)</span>.  Then</p>
<div class="math notranslate nohighlight">
\[\begin{split}3a+1&amp;\le 3\cdot 2+1\\
&amp;=7.\end{split}\]</div>
</div>
<p>In handwritten work, it is quite common to annotate the two directions with the symbols
<span class="math notranslate nohighlight">\(\Rightarrow\)</span> and <span class="math notranslate nohighlight">\(\Leftarrow\)</span> respectively:</p>
<div class="admonition-solution admonition">
<p class="admonition-title">Solution</p>
<p><span class="math notranslate nohighlight">\(\Rightarrow\)</span> Suppose that <span class="math notranslate nohighlight">\(3a+1\le 7\)</span>. Then &#8230;</p>
<p><span class="math notranslate nohighlight">\(\Leftarrow\)</span> Suppose that <span class="math notranslate nohighlight">\(a\le 2\)</span>.  Then &#8230;</p>
</div>
<p>This is recommended for homework, tests, writing on the blackboard, etc.  In more formal writing
(such as this book) we omit such symbols and instead use words like &#8220;First&#8221; and
&#8220;Conversely&#8221; to signal the different parts of the proof.</p>
<p>In Lean, an &#8220;if and only if&#8221; is stated with the bi-implication symbol <code class="docutils literal notranslate"><span class="pre">&#8596;</span></code>.  Since, under the hood,
an &#8220;if and only if&#8221; is an &#8220;and&#8221; statement, we use the same tactic as for &#8220;and&#8221; goals:
<code class="docutils literal notranslate"><span class="pre">constructor</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">{</span><span class="n">a</span> <span class="o">:</span> <span class="n">&#8474;</span><span class="o">}</span> <span class="o">:</span> <span class="mi">3</span> <span class="bp">*</span> <span class="n">a</span> <span class="bp">+</span> <span class="mi">1</span> <span class="bp">&#8804;</span> <span class="mi">7</span> <span class="bp">&#8596;</span> <span class="n">a</span> <span class="bp">&#8804;</span> <span class="mi">2</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">constructor</span>
  <span class="bp">&#183;</span> <span class="n">intro</span> <span class="n">h</span>
    <span class="k">calc</span> <span class="n">a</span> <span class="bp">=</span> <span class="o">((</span><span class="mi">3</span> <span class="bp">*</span> <span class="n">a</span> <span class="bp">+</span> <span class="mi">1</span><span class="o">)</span> <span class="bp">-</span> <span class="mi">1</span><span class="o">)</span> <span class="bp">/</span> <span class="mi">3</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">ring</span>
      <span class="n">_</span> <span class="bp">&#8804;</span> <span class="o">(</span><span class="mi">7</span> <span class="bp">-</span> <span class="mi">1</span><span class="o">)</span> <span class="bp">/</span> <span class="mi">3</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">rel</span> <span class="o">[</span><span class="n">h</span><span class="o">]</span>
      <span class="n">_</span> <span class="bp">=</span> <span class="mi">2</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">numbers</span>
  <span class="bp">&#183;</span> <span class="n">intro</span> <span class="n">h</span>
    <span class="k">calc</span> <span class="mi">3</span> <span class="bp">*</span> <span class="n">a</span> <span class="bp">+</span> <span class="mi">1</span> <span class="bp">&#8804;</span> <span class="mi">3</span> <span class="bp">*</span> <span class="mi">2</span> <span class="bp">+</span> <span class="mi">1</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">rel</span> <span class="o">[</span><span class="n">h</span><span class="o">]</span>
      <span class="n">_</span> <span class="bp">=</span> <span class="mi">7</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">numbers</span>
</pre></div>
</div>
</section>
<section id="bezout-iff">
<span id="id13"></span><h3><span class="section-number">4.2.2. </span>Example<a class="headerlink" href="#bezout-iff" title="Permalink to this headline">&#61633;</a></h3>
<p>Let&#8217;s modify <a class="reference internal" href="03_Parity_and_Divisibility.html#bezout-prob1"><span class="std std-numref">Example 3.5.1</span></a> to be an if-and-only-if problem.  Now there are two
things to prove, one of which we did before.</p>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Let <span class="math notranslate nohighlight">\(n\)</span> be an integer. Show that <span class="math notranslate nohighlight">\(5n\)</span> is a multiple of <span class="math notranslate nohighlight">\(8\)</span> if and only if
<span class="math notranslate nohighlight">\(n\)</span> is.</p>
</div>
<div class="admonition-solution admonition">
<p class="admonition-title">Solution</p>
<p>Suppose that <span class="math notranslate nohighlight">\(8\mid 5n\)</span>. Then there exists an integer <span class="math notranslate nohighlight">\(a\)</span> such that <span class="math notranslate nohighlight">\(5n=8a\)</span>.
So</p>
<div class="math notranslate nohighlight">
\[\begin{split}n &amp;= -3  (5  n) + 16 n \\
&amp;= -3  (8  a) + 16  n \\
&amp; = 8 (-3 a + 2  n),\end{split}\]</div>
<p>so <span class="math notranslate nohighlight">\(8\mid n\)</span>.</p>
<p>Conversely, suppose that <span class="math notranslate nohighlight">\(8\mid n\)</span>. Then there exists an integer <span class="math notranslate nohighlight">\(a\)</span> such that
<span class="math notranslate nohighlight">\(n=8a\)</span>. So</p>
<div class="math notranslate nohighlight">
\[\begin{split}5n &amp;= 5(8a) \\
&amp;= 8(5a),\end{split}\]</div>
<p>so <span class="math notranslate nohighlight">\(8\mid 5n\)</span>.</p>
</div>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">{</span><span class="n">n</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">}</span> <span class="o">:</span> <span class="mi">8</span> <span class="bp">&#8739;</span> <span class="mi">5</span> <span class="bp">*</span> <span class="n">n</span> <span class="bp">&#8596;</span> <span class="mi">8</span> <span class="bp">&#8739;</span> <span class="n">n</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">constructor</span>
  <span class="bp">&#183;</span> <span class="n">intro</span> <span class="n">hn</span>
    <span class="n">obtain</span> <span class="o">&#10216;</span><span class="n">a</span><span class="o">,</span> <span class="n">ha</span><span class="o">&#10217;</span> <span class="o">:=</span> <span class="n">hn</span>
    <span class="n">use</span> <span class="bp">-</span><span class="mi">3</span> <span class="bp">*</span> <span class="n">a</span> <span class="bp">+</span> <span class="mi">2</span> <span class="bp">*</span> <span class="n">n</span>
    <span class="k">calc</span>
      <span class="n">n</span> <span class="bp">=</span> <span class="bp">-</span><span class="mi">3</span> <span class="bp">*</span> <span class="o">(</span><span class="mi">5</span> <span class="bp">*</span> <span class="n">n</span><span class="o">)</span> <span class="bp">+</span> <span class="mi">16</span> <span class="bp">*</span> <span class="n">n</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">ring</span>
      <span class="n">_</span> <span class="bp">=</span> <span class="bp">-</span><span class="mi">3</span> <span class="bp">*</span> <span class="o">(</span><span class="mi">8</span> <span class="bp">*</span> <span class="n">a</span><span class="o">)</span> <span class="bp">+</span> <span class="mi">16</span> <span class="bp">*</span> <span class="n">n</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">rw</span> <span class="o">[</span><span class="n">ha</span><span class="o">]</span>
      <span class="n">_</span> <span class="bp">=</span> <span class="mi">8</span> <span class="bp">*</span> <span class="o">(</span><span class="bp">-</span><span class="mi">3</span> <span class="bp">*</span> <span class="n">a</span> <span class="bp">+</span> <span class="mi">2</span> <span class="bp">*</span> <span class="n">n</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">ring</span>
  <span class="bp">&#183;</span> <span class="n">intro</span> <span class="n">hn</span>
    <span class="n">obtain</span> <span class="o">&#10216;</span><span class="n">a</span><span class="o">,</span> <span class="n">ha</span><span class="o">&#10217;</span> <span class="o">:=</span> <span class="n">hn</span>
    <span class="n">use</span> <span class="mi">5</span> <span class="bp">*</span> <span class="n">a</span>
    <span class="k">calc</span> <span class="mi">5</span> <span class="bp">*</span> <span class="n">n</span> <span class="bp">=</span> <span class="mi">5</span> <span class="bp">*</span> <span class="o">(</span><span class="mi">8</span> <span class="bp">*</span> <span class="n">a</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">rw</span> <span class="o">[</span><span class="n">ha</span><span class="o">]</span>
      <span class="n">_</span> <span class="bp">=</span> <span class="mi">8</span> <span class="bp">*</span> <span class="o">(</span><span class="mi">5</span> <span class="bp">*</span> <span class="n">a</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">ring</span>
</pre></div>
</div>
</section>
<section id="odd-iff-modeq">
<span id="id14"></span><h3><span class="section-number">4.2.3. </span>Example<a class="headerlink" href="#odd-iff-modeq" title="Permalink to this headline">&#61633;</a></h3>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Show that an integer <span class="math notranslate nohighlight">\(n\)</span> is odd, if and only if it is congruent to 1 modulo 2.</p>
</div>
<div class="admonition-solution admonition">
<p class="admonition-title">Solution</p>
<p>First, suppose that <span class="math notranslate nohighlight">\(n\)</span> is odd.  Then there exists an integer <span class="math notranslate nohighlight">\(k\)</span> such that
<span class="math notranslate nohighlight">\(n=2k+1\)</span>.  Therefore <span class="math notranslate nohighlight">\(n-1=2k\)</span>, so <span class="math notranslate nohighlight">\(n-1\)</span> is divisible by 2, so
<span class="math notranslate nohighlight">\(n\equiv 1\mod 2\)</span>.</p>
<p>Conversely, suppose that <span class="math notranslate nohighlight">\(n\equiv 1\mod 2\)</span>.  Then <span class="math notranslate nohighlight">\(2\mid n -1\)</span>, so there exists an
integer <span class="math notranslate nohighlight">\(k\)</span> such <span class="math notranslate nohighlight">\(n-1=2k\)</span>.  Thus <span class="math notranslate nohighlight">\(n=2k+1\)</span> and so <span class="math notranslate nohighlight">\(n\)</span> is odd.</p>
</div>
<p>We name this example <code class="docutils literal notranslate"><span class="pre">Int.odd_iff_modEq</span></code> for future use.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">theorem</span> <span class="n">odd_iff_modEq</span> <span class="o">(</span><span class="n">n</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">)</span> <span class="o">:</span> <span class="n">Odd</span> <span class="n">n</span> <span class="bp">&#8596;</span> <span class="n">n</span> <span class="bp">&#8801;</span> <span class="mi">1</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="mi">2</span><span class="o">]</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">constructor</span>
  <span class="bp">&#183;</span> <span class="n">intro</span> <span class="n">h</span>
    <span class="n">obtain</span> <span class="o">&#10216;</span><span class="n">k</span><span class="o">,</span> <span class="n">hk</span><span class="o">&#10217;</span> <span class="o">:=</span> <span class="n">h</span>
    <span class="n">dsimp</span> <span class="o">[</span><span class="n">Int.ModEq</span><span class="o">]</span>
    <span class="n">dsimp</span> <span class="o">[(</span><span class="bp">&#183;</span> <span class="bp">&#8739;</span> <span class="bp">&#183;</span><span class="o">)]</span>
    <span class="n">use</span> <span class="n">k</span>
    <span class="n">addarith</span> <span class="o">[</span><span class="n">hk</span><span class="o">]</span>
  <span class="bp">&#183;</span> <span class="gr">sorry</span>
</pre></div>
</div>
</section>
<section id="even-iff-modeq">
<span id="id15"></span><h3><span class="section-number">4.2.4. </span>Example<a class="headerlink" href="#even-iff-modeq" title="Permalink to this headline">&#61633;</a></h3>
<p>Now do the same to characterise evenness.</p>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Show that an integer <span class="math notranslate nohighlight">\(n\)</span> is even, if and only if it is congruent to 0 modulo 2.</p>
</div>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">theorem</span> <span class="n">even_iff_modEq</span> <span class="o">(</span><span class="n">n</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">)</span> <span class="o">:</span> <span class="n">Even</span> <span class="n">n</span> <span class="bp">&#8596;</span> <span class="n">n</span> <span class="bp">&#8801;</span> <span class="mi">0</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="mi">2</span><span class="o">]</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">constructor</span>
  <span class="bp">&#183;</span> <span class="n">intro</span> <span class="n">h</span>
    <span class="n">obtain</span> <span class="o">&#10216;</span><span class="n">k</span><span class="o">,</span> <span class="n">hk</span><span class="o">&#10217;</span> <span class="o">:=</span> <span class="n">h</span>
    <span class="n">dsimp</span> <span class="o">[</span><span class="n">Int.ModEq</span><span class="o">]</span>
    <span class="n">dsimp</span> <span class="o">[(</span><span class="bp">&#183;</span> <span class="bp">&#8739;</span> <span class="bp">&#183;</span><span class="o">)]</span>
    <span class="n">use</span> <span class="n">k</span>
    <span class="n">addarith</span> <span class="o">[</span><span class="n">hk</span><span class="o">]</span>
  <span class="bp">&#183;</span> <span class="gr">sorry</span>
</pre></div>
</div>
</section>
<section id="id16">
<h3><span class="section-number">4.2.5. </span>Example<a class="headerlink" href="#id16" title="Permalink to this headline">&#61633;</a></h3>
<p>The high school concept of &#8220;solving&#8221; equations represents an &#8220;if and only if&#8221; problem: to solve an
equation, you state a list of numbers and prove that they satisfy the equation and no other numbers
do.</p>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Let <span class="math notranslate nohighlight">\(x\)</span> be a real number.  Show that <span class="math notranslate nohighlight">\(x ^ 2 + x - 6 = 0\)</span>, if and only if <span class="math notranslate nohighlight">\(x = -3\)</span>
or <span class="math notranslate nohighlight">\(x = 2\)</span>.</p>
</div>
<div class="admonition-solution admonition">
<p class="admonition-title">Solution</p>
<p>First, suppose that <span class="math notranslate nohighlight">\(x ^ 2 + x - 6 = 0\)</span>.  Then</p>
<div class="math notranslate nohighlight">
\[\begin{split}(x+3)(x-2)&amp;=x ^ 2 + x - 6\\
&amp;=0,\end{split}\]</div>
<p>so either <span class="math notranslate nohighlight">\(x+3=0\)</span> or <span class="math notranslate nohighlight">\(x-2=0\)</span>.  If the former, <span class="math notranslate nohighlight">\(x=-3\)</span>; if the latter,
<span class="math notranslate nohighlight">\(x=2\)</span>.</p>
<p>Conversely, if <span class="math notranslate nohighlight">\(x=-3\)</span> then</p>
<div class="math notranslate nohighlight">
\[\begin{split}x ^ 2 + x - 6&amp;=(-3)^2+(-3)-6\\
&amp;=0,\end{split}\]</div>
<p>and if <span class="math notranslate nohighlight">\(x=2\)</span> then</p>
<div class="math notranslate nohighlight">
\[\begin{split}x ^ 2 + x - 6&amp;=2^2+2-6\\
&amp;=0.\end{split}\]</div>
</div>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">{</span><span class="n">x</span> <span class="o">:</span> <span class="n">&#8477;</span><span class="o">}</span> <span class="o">:</span> <span class="n">x</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">+</span> <span class="n">x</span> <span class="bp">-</span> <span class="mi">6</span> <span class="bp">=</span> <span class="mi">0</span> <span class="bp">&#8596;</span> <span class="n">x</span> <span class="bp">=</span> <span class="bp">-</span><span class="mi">3</span> <span class="bp">&#8744;</span> <span class="n">x</span> <span class="bp">=</span> <span class="mi">2</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</section>
<section id="id17">
<h3><span class="section-number">4.2.6. </span>Example<a class="headerlink" href="#id17" title="Permalink to this headline">&#61633;</a></h3>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Let <span class="math notranslate nohighlight">\(a\)</span> be an integer.  Show that <span class="math notranslate nohighlight">\(a^2-5a+5 \le -1\)</span>, if and only if <span class="math notranslate nohighlight">\(a\)</span> is 2
or 3.</p>
</div>
<div class="admonition-solution admonition">
<p class="admonition-title">Solution</p>
<p>First, suppose that <span class="math notranslate nohighlight">\(a^2-5a+5 \le -1\)</span>.  Then</p>
<div class="math notranslate nohighlight">
\[\begin{split}(2 a - 5) ^ 2&amp;= 4 (a ^ 2 - 5 a + 5) + 5 \\
&amp;\le 4 \cdot -1 + 5 \\
&amp;= 1^2,\end{split}\]</div>
<p>so <span class="math notranslate nohighlight">\(-1\le 2a-5\le 1\)</span>.  Therefore <span class="math notranslate nohighlight">\(2 \cdot 2 \le 2a\)</span>, so <span class="math notranslate nohighlight">\(2 \le a\)</span>, and similarly
<span class="math notranslate nohighlight">\(2a  &#8804; 2 \cdot 3\)</span>, so <span class="math notranslate nohighlight">\(a \le 3\)</span>.  Since <span class="math notranslate nohighlight">\(2\le a\le 3\)</span>, <span class="math notranslate nohighlight">\(a\)</span> is 2 or 3.</p>
<p>Conversely, if <span class="math notranslate nohighlight">\(a=2\)</span> then</p>
<div class="math notranslate nohighlight">
\[\begin{split}a^2-5a+5 &amp;= 2^2-5\cdot 2+5  \\
&amp;\le -1,\end{split}\]</div>
<p>and if <span class="math notranslate nohighlight">\(a=3\)</span> then</p>
<div class="math notranslate nohighlight">
\[\begin{split}a^2-5a+5 &amp;= 3^2-5\cdot 3+5  \\
&amp;\le -1.\end{split}\]</div>
</div>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">{</span><span class="n">a</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">}</span> <span class="o">:</span> <span class="n">a</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">-</span> <span class="mi">5</span> <span class="bp">*</span> <span class="n">a</span> <span class="bp">+</span> <span class="mi">5</span> <span class="bp">&#8804;</span> <span class="bp">-</span><span class="mi">1</span> <span class="bp">&#8596;</span> <span class="n">a</span> <span class="bp">=</span> <span class="mi">2</span> <span class="bp">&#8744;</span> <span class="n">a</span> <span class="bp">=</span> <span class="mi">3</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</section>
<section id="id18">
<h3><span class="section-number">4.2.7. </span>Example<a class="headerlink" href="#id18" title="Permalink to this headline">&#61633;</a></h3>
<p>Some library lemmas have the form of an &#8220;if and only if&#8221;.  This is convenient because they take
the place of two ordinary lemmas, one for each direction.</p>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Let <span class="math notranslate nohighlight">\(n\)</span> be an integer and suppose <span class="math notranslate nohighlight">\(n ^ 2 - 10 n + 24 = 0\)</span>.  Show that <span class="math notranslate nohighlight">\(n\)</span> is
even.</p>
</div>
<div class="admonition-solution admonition">
<p class="admonition-title">Solution</p>
<p>We have</p>
<div class="math notranslate nohighlight">
\[\begin{split}(n-4)(n-6)&amp;= n^2-10n+24\\
&amp;= 0,\end{split}\]</div>
<p>so either <span class="math notranslate nohighlight">\(n-4=0\)</span> or <span class="math notranslate nohighlight">\(n-6=0\)</span>.  If the former, then <span class="math notranslate nohighlight">\(n=2\cdot 2\)</span> so <span class="math notranslate nohighlight">\(n\)</span> is
even; if the latter, then <span class="math notranslate nohighlight">\(n=2\cdot 3\)</span> so <span class="math notranslate nohighlight">\(n\)</span> is even.</p>
</div>
<p>In this problem we need to transform the fact <span class="math notranslate nohighlight">\((n-4)(n-6)=0\)</span> into the fact that
&#8220;<span class="math notranslate nohighlight">\(n-4=0\)</span> or <span class="math notranslate nohighlight">\(n-6=0\)</span>.&#8221;  Previously (like in <a class="reference internal" href="02_Proofs_with_Structure.html#solve-quadratic"><span class="std std-numref">Example 2.3.4</span></a>), we
would have done this in Lean by inserting this fact directly into the lemma</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">theorem</span> <span class="n">eq_zero_or_eq_zero_of_mul_eq_zero</span> <span class="o">{</span><span class="n">a</span> <span class="n">b</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">}</span> <span class="o">(</span><span class="n">h</span> <span class="o">:</span> <span class="n">a</span> <span class="bp">*</span> <span class="n">b</span> <span class="bp">=</span> <span class="mi">0</span><span class="o">)</span> <span class="o">:</span> <span class="n">a</span> <span class="bp">=</span> <span class="mi">0</span> <span class="bp">&#8744;</span> <span class="n">b</span> <span class="bp">=</span> <span class="mi">0</span> <span class="o">:=</span>
</pre></div>
</div>
<p>resulting in a proof setup like this:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">{</span><span class="n">n</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">}</span> <span class="o">(</span><span class="n">hn</span> <span class="o">:</span> <span class="n">n</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">-</span> <span class="mi">10</span> <span class="bp">*</span> <span class="n">n</span> <span class="bp">+</span> <span class="mi">24</span> <span class="bp">=</span> <span class="mi">0</span><span class="o">)</span> <span class="o">:</span> <span class="n">Even</span> <span class="n">n</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="k">have</span> <span class="n">hn1</span> <span class="o">:=</span>
    <span class="k">calc</span> <span class="o">(</span><span class="n">n</span> <span class="bp">-</span> <span class="mi">4</span><span class="o">)</span> <span class="bp">*</span> <span class="o">(</span><span class="n">n</span> <span class="bp">-</span> <span class="mi">6</span><span class="o">)</span> <span class="bp">=</span> <span class="n">n</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">-</span> <span class="mi">10</span> <span class="bp">*</span> <span class="n">n</span> <span class="bp">+</span> <span class="mi">24</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">ring</span>
      <span class="n">_</span> <span class="bp">=</span> <span class="mi">0</span> <span class="o">:=</span> <span class="n">hn</span>
  <span class="k">have</span> <span class="n">hn2</span> <span class="o">:=</span> <span class="n">eq_zero_or_eq_zero_of_mul_eq_zero</span> <span class="n">hn1</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
<p>(Exercise: finish off the proof.)</p>
<p>But there is also a library lemma in <code class="docutils literal notranslate"><span class="pre">&#8596;</span></code> form, which combines <code class="docutils literal notranslate"><span class="pre">eq_zero_or_eq_zero_of_mul_eq_zero</span></code>
with the <em>converse</em> (other direction) of that statement:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">theorem</span> <span class="n">mul_eq_zero</span> <span class="o">{</span><span class="n">a</span> <span class="n">b</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">}</span> <span class="o">:</span> <span class="n">a</span> <span class="bp">*</span> <span class="n">b</span> <span class="bp">=</span> <span class="mi">0</span> <span class="bp">&#8596;</span> <span class="n">a</span> <span class="bp">=</span> <span class="mi">0</span> <span class="bp">&#8744;</span> <span class="n">b</span> <span class="bp">=</span> <span class="mi">0</span> <span class="o">:=</span>
</pre></div>
</div>
<p>We can use an <code class="docutils literal notranslate"><span class="pre">&#8596;</span></code> lemma in Lean with the <code class="docutils literal notranslate"><span class="pre">rw</span></code> tactic; it converts a hypothesis (or the goal) in
the form of the left-hand side of the <code class="docutils literal notranslate"><span class="pre">&#8596;</span></code> to one with the form of the right-hand side.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">{</span><span class="n">n</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">}</span> <span class="o">(</span><span class="n">hn</span> <span class="o">:</span> <span class="n">n</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">-</span> <span class="mi">10</span> <span class="bp">*</span> <span class="n">n</span> <span class="bp">+</span> <span class="mi">24</span> <span class="bp">=</span> <span class="mi">0</span><span class="o">)</span> <span class="o">:</span> <span class="n">Even</span> <span class="n">n</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="k">have</span> <span class="n">hn1</span> <span class="o">:=</span>
    <span class="k">calc</span> <span class="o">(</span><span class="n">n</span> <span class="bp">-</span> <span class="mi">4</span><span class="o">)</span> <span class="bp">*</span> <span class="o">(</span><span class="n">n</span> <span class="bp">-</span> <span class="mi">6</span><span class="o">)</span> <span class="bp">=</span> <span class="n">n</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">-</span> <span class="mi">10</span> <span class="bp">*</span> <span class="n">n</span> <span class="bp">+</span> <span class="mi">24</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">ring</span>
      <span class="n">_</span> <span class="bp">=</span> <span class="mi">0</span> <span class="o">:=</span> <span class="n">hn</span>
  <span class="n">rw</span> <span class="o">[</span><span class="n">mul_eq_zero</span><span class="o">]</span> <span class="n">at</span> <span class="n">hn1</span> <span class="c1">-- `hn1 : n - 4 = 0 &#8744; n - 6 = 0`</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</section>
<section id="id19">
<h3><span class="section-number">4.2.8. </span>Example<a class="headerlink" href="#id19" title="Permalink to this headline">&#61633;</a></h3>
<p>Above, in <a class="reference internal" href="#odd-iff-modeq"><span class="std std-numref">Example 4.2.3</span></a>, we proved that an integer is odd if and only if it
is congruent to 1 modulo 2, recording this under the name <code class="docutils literal notranslate"><span class="pre">Int.odd_iff_modEq</span></code>.  This is now also
a convenient &#8220;if and only if&#8221; library lemma which we can use to  solve problems about parity using
modulo arithmetic.  As an example, let&#8217;s re-do the problem from
<a class="reference internal" href="03_Parity_and_Divisibility.html#typical-parity"><span class="std std-numref">Example 3.1.5</span></a>.</p>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Prove that if the integers <span class="math notranslate nohighlight">\(x\)</span> and <span class="math notranslate nohighlight">\(y\)</span> are odd, then <span class="math notranslate nohighlight">\(x+y+1\)</span> is odd.</p>
</div>
<div class="admonition-solution admonition">
<p class="admonition-title">Solution</p>
<p>We will prove that if <span class="math notranslate nohighlight">\(x\equiv 1 \mod 2\)</span> and <span class="math notranslate nohighlight">\(y\equiv 1 \mod 2\)</span> then
<span class="math notranslate nohighlight">\(x+y+1\equiv 1 \mod 2\)</span>.  Indeed,</p>
<div class="math notranslate nohighlight">
\[\begin{split}x + y + 1 &amp;\equiv 1 + 1 + 1 \mod 2\\
&amp;= 2 \cdot 1 + 1\\
&amp;\equiv 1\mod 2.\end{split}\]</div>
</div>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">{</span><span class="n">x</span> <span class="n">y</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">}</span> <span class="o">(</span><span class="n">hx</span> <span class="o">:</span> <span class="n">Odd</span> <span class="n">x</span><span class="o">)</span> <span class="o">(</span><span class="n">hy</span> <span class="o">:</span> <span class="n">Odd</span> <span class="n">y</span><span class="o">)</span> <span class="o">:</span> <span class="n">Odd</span> <span class="o">(</span><span class="n">x</span> <span class="bp">+</span> <span class="n">y</span> <span class="bp">+</span> <span class="mi">1</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">rw</span> <span class="o">[</span><span class="n">Int.odd_iff_modEq</span><span class="o">]</span> <span class="n">at</span> <span class="bp">*</span>
  <span class="k">calc</span> <span class="n">x</span> <span class="bp">+</span> <span class="n">y</span> <span class="bp">+</span> <span class="mi">1</span> <span class="bp">&#8801;</span> <span class="mi">1</span> <span class="bp">+</span> <span class="mi">1</span> <span class="bp">+</span> <span class="mi">1</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="mi">2</span><span class="o">]</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">rel</span> <span class="o">[</span><span class="n">hx</span><span class="o">,</span> <span class="n">hy</span><span class="o">]</span>
    <span class="n">_</span> <span class="bp">=</span> <span class="mi">2</span> <span class="bp">*</span> <span class="mi">1</span> <span class="bp">+</span> <span class="mi">1</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">ring</span>
    <span class="n">_</span> <span class="bp">&#8801;</span> <span class="mi">1</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="mi">2</span><span class="o">]</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">extra</span>
</pre></div>
</div>
</section>
<section id="even-or-odd-proof">
<span id="id20"></span><h3><span class="section-number">4.2.9. </span>Example<a class="headerlink" href="#even-or-odd-proof" title="Permalink to this headline">&#61633;</a></h3>
<p>Another way we can use the characterization of parity in terms of modular arithmetic is to
prove the theorem from <a class="reference internal" href="03_Parity_and_Divisibility.html#even-or-odd"><span class="std std-numref">Example 3.1.9</span></a> whose proof we skipped.</p>
<div class="admonition-theorem admonition">
<p class="admonition-title">Theorem</p>
<p>Every integer is either even or odd.</p>
</div>
<div class="admonition-proof admonition">
<p class="admonition-title">Proof</p>
<p>Let <span class="math notranslate nohighlight">\(n\)</span> be an integer.  We do a case division according to the residue of <span class="math notranslate nohighlight">\(n\)</span>
modulo 2.</p>
<p>If <span class="math notranslate nohighlight">\(n\equiv 0\mod 2\)</span>, then <span class="math notranslate nohighlight">\(n\)</span> is even, and we are done.</p>
<p>If <span class="math notranslate nohighlight">\(n\equiv 0\mod 2\)</span>, then <span class="math notranslate nohighlight">\(n\)</span> is odd, and we are done.</p>
</div>
<p>Write this in Lean using the lemmas <code class="docutils literal notranslate"><span class="pre">Int.odd_iff_modEq</span></code> and <code class="docutils literal notranslate"><span class="pre">Int.even_iff_modEq</span></code> from
<a class="reference internal" href="#odd-iff-modeq"><span class="std std-numref">Example 4.2.3</span></a> and <a class="reference internal" href="#even-iff-modeq"><span class="std std-numref">Example 4.2.4</span></a>, together with the
tactic <code class="docutils literal notranslate"><span class="pre">mod_cases</span></code>.  I have written the beginning.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">(</span><span class="n">n</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">)</span> <span class="o">:</span> <span class="n">Even</span> <span class="n">n</span> <span class="bp">&#8744;</span> <span class="n">Odd</span> <span class="n">n</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">mod_cases</span> <span class="n">hn</span> <span class="o">:</span> <span class="n">n</span> <span class="bp">%</span> <span class="mi">2</span>
  <span class="bp">&#183;</span> <span class="n">left</span>
    <span class="n">rw</span> <span class="o">[</span><span class="n">Int.even_iff_modEq</span><span class="o">]</span>
    <span class="n">apply</span> <span class="n">hn</span>
  <span class="bp">&#183;</span> <span class="gr">sorry</span>
</pre></div>
</div>
</section>
<section id="id21">
<h3><span class="section-number">4.2.10. </span>Exercises<a class="headerlink" href="#id21" title="Permalink to this headline">&#61633;</a></h3>
<ol class="arabic">
<li><p>Let <span class="math notranslate nohighlight">\(x\)</span> be a real number.  Show that <span class="math notranslate nohighlight">\(2x-1=11\)</span> if and only if <span class="math notranslate nohighlight">\(x=6\)</span>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">{</span><span class="n">x</span> <span class="o">:</span> <span class="n">&#8477;</span><span class="o">}</span> <span class="o">:</span> <span class="mi">2</span> <span class="bp">*</span> <span class="n">x</span> <span class="bp">-</span> <span class="mi">1</span> <span class="bp">=</span> <span class="mi">11</span> <span class="bp">&#8596;</span> <span class="n">x</span> <span class="bp">=</span> <span class="mi">6</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Let <span class="math notranslate nohighlight">\(n\)</span> be an integer. Show that 63 is a factor of <span class="math notranslate nohighlight">\(n\)</span> if and only if both 7 and 9
are.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">{</span><span class="n">n</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">}</span> <span class="o">:</span> <span class="mi">63</span> <span class="bp">&#8739;</span> <span class="n">n</span> <span class="bp">&#8596;</span> <span class="mi">7</span> <span class="bp">&#8739;</span> <span class="n">n</span> <span class="bp">&#8743;</span> <span class="mi">9</span> <span class="bp">&#8739;</span> <span class="n">n</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Let <span class="math notranslate nohighlight">\(a\)</span> and <span class="math notranslate nohighlight">\(n\)</span> be integers. Show that <span class="math notranslate nohighlight">\(a\)</span> is a multiple of <span class="math notranslate nohighlight">\(n\)</span> if and
only if <span class="math notranslate nohighlight">\(a \equiv 0 \mod n\)</span>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">theorem</span> <span class="n">dvd_iff_modEq</span> <span class="o">{</span><span class="n">a</span> <span class="n">n</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">}</span> <span class="o">:</span> <span class="n">n</span> <span class="bp">&#8739;</span> <span class="n">a</span> <span class="bp">&#8596;</span> <span class="n">a</span> <span class="bp">&#8801;</span> <span class="mi">0</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="n">n</span><span class="o">]</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Let <span class="math notranslate nohighlight">\(a\)</span> and <span class="math notranslate nohighlight">\(b\)</span> be integers and suppose that <span class="math notranslate nohighlight">\(a \mid b\)</span>.  Show that
<span class="math notranslate nohighlight">\(a \mid 2b^3-b^2+3b\)</span>.</p>
<p>Note that this appeared already as an exercise in <a class="reference internal" href="03_Parity_and_Divisibility.html#divisibility"><span class="std std-numref">Section 3.2</span></a>.  But now,
using the lemma <code class="docutils literal notranslate"><span class="pre">Int.dvd_iff_modEq</span></code> proved in the previous exercise, this kind of problem is
much easier.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">{</span><span class="n">a</span> <span class="n">b</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">}</span> <span class="o">(</span><span class="n">hab</span> <span class="o">:</span> <span class="n">a</span> <span class="bp">&#8739;</span> <span class="n">b</span><span class="o">)</span> <span class="o">:</span> <span class="n">a</span> <span class="bp">&#8739;</span> <span class="mi">2</span> <span class="bp">*</span> <span class="n">b</span> <span class="bp">^</span> <span class="mi">3</span> <span class="bp">-</span> <span class="n">b</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">+</span> <span class="mi">3</span> <span class="bp">*</span> <span class="n">b</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Let <span class="math notranslate nohighlight">\(k\)</span> be a natural number.  Show that <span class="math notranslate nohighlight">\(k^2 \le 6\)</span>, if and only if <span class="math notranslate nohighlight">\(k\)</span> is 0, 1
or 2.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">{</span><span class="n">k</span> <span class="o">:</span> <span class="n">&#8469;</span><span class="o">}</span> <span class="o">:</span> <span class="n">k</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">&#8804;</span> <span class="mi">6</span> <span class="bp">&#8596;</span> <span class="n">k</span> <span class="bp">=</span> <span class="mi">0</span> <span class="bp">&#8744;</span> <span class="n">k</span> <span class="bp">=</span> <span class="mi">1</span> <span class="bp">&#8744;</span> <span class="n">k</span> <span class="bp">=</span> <span class="mi">2</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
</ol>
</section>
</section>
<section id="there-exists-a-unique">
<span id="exists-unique"></span><h2><span class="section-number">4.3. </span>&#8220;There exists a unique&#8221;<a class="headerlink" href="#there-exists-a-unique" title="Permalink to this headline">&#61633;</a></h2>
<section id="id22">
<h3><span class="section-number">4.3.1. </span>Example<a class="headerlink" href="#id22" title="Permalink to this headline">&#61633;</a></h3>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Show that there exists a unique real number <span class="math notranslate nohighlight">\(a\)</span>, such that <span class="math notranslate nohighlight">\(3a+1=7\)</span>.</p>
</div>
<div class="admonition-solution admonition">
<p class="admonition-title">Solution</p>
<p>We will show that 2 is the unique real number with this property.</p>
<p>First, we show that 2 has this property.  Indeed, <span class="math notranslate nohighlight">\(3\cdot 2+1=7\)</span>.</p>
<p>Now, let <span class="math notranslate nohighlight">\(y\)</span> be a real number for which <span class="math notranslate nohighlight">\(3y+1=7\)</span>.  Then</p>
<div class="math notranslate nohighlight">
\[\begin{split}y &amp;= \frac{(3 y + 1) - 1} {3}\\
&amp;= \frac{7 - 1}{ 3}\\
&amp;= 2.\end{split}\]</div>
</div>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="bp">&#8707;!</span> <span class="n">a</span> <span class="o">:</span> <span class="n">&#8477;</span><span class="o">,</span> <span class="mi">3</span> <span class="bp">*</span> <span class="n">a</span> <span class="bp">+</span> <span class="mi">1</span> <span class="bp">=</span> <span class="mi">7</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">use</span> <span class="mi">2</span>
  <span class="n">dsimp</span>
  <span class="n">constructor</span>
  <span class="bp">&#183;</span> <span class="n">numbers</span>
  <span class="n">intro</span> <span class="n">y</span> <span class="n">hy</span>
  <span class="k">calc</span>
    <span class="n">y</span> <span class="bp">=</span> <span class="o">(</span><span class="mi">3</span> <span class="bp">*</span> <span class="n">y</span> <span class="bp">+</span> <span class="mi">1</span> <span class="bp">-</span> <span class="mi">1</span><span class="o">)</span> <span class="bp">/</span> <span class="mi">3</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">ring</span>
    <span class="n">_</span> <span class="bp">=</span> <span class="o">(</span><span class="mi">7</span> <span class="bp">-</span> <span class="mi">1</span><span class="o">)</span> <span class="bp">/</span> <span class="mi">3</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">rw</span> <span class="o">[</span><span class="n">hy</span><span class="o">]</span>
    <span class="n">_</span> <span class="bp">=</span> <span class="mi">2</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">numbers</span>
</pre></div>
</div>
</section>
<section id="id23">
<h3><span class="section-number">4.3.2. </span>Example<a class="headerlink" href="#id23" title="Permalink to this headline">&#61633;</a></h3>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Show that there exists a unique rational number <span class="math notranslate nohighlight">\(x\)</span>, such that for every rational number
<span class="math notranslate nohighlight">\(a\)</span> between 1 and 3, <span class="math notranslate nohighlight">\((a-x)^2\le 1\)</span>.</p>
</div>
<div class="admonition-solution admonition">
<p class="admonition-title">Solution</p>
<p>We will show that 2 is the unique rational number with this property.</p>
<p>Firstly, if <span class="math notranslate nohighlight">\(a\)</span> is a rational number between 1 and 3, then <span class="math notranslate nohighlight">\(-1 \le a-2 \le 1\)</span>, so by
<a class="reference internal" href="02_Proofs_with_Structure.html#prove-sq-le-sq"><span class="std std-numref">Example 2.1.7</span></a>,</p>
<div class="math notranslate nohighlight">
\[\begin{split}(a-2)^2 &amp;\le 1 ^ 2\\
&amp;=1.\end{split}\]</div>
<p>Now, let <span class="math notranslate nohighlight">\(y\)</span> be a rational number for which,  for every rational number
<span class="math notranslate nohighlight">\(a\)</span> between 1 and 3, <span class="math notranslate nohighlight">\((a-y)^2\le 1\)</span>.</p>
<p>Since 1 is between 1 and 3, <span class="math notranslate nohighlight">\((1-y)^2\le 1\)</span>, and since 3 is between 1 and 3,
<span class="math notranslate nohighlight">\((3-y)^2\le 1\)</span>.</p>
<p>So</p>
<div class="math notranslate nohighlight">
\[\begin{split}(y - 2) ^ 2 &amp;= \frac{(1 - y) ^ 2 + (3 - y) ^ 2 - 2}{ 2}\\
&amp;&#8804;  \frac{1 + 1 - 2}{2} \\
&amp; = 0.\end{split}\]</div>
<p>Also <span class="math notranslate nohighlight">\((y - 2) ^ 2\geq 0\)</span>, since squares are positive.  Thus
<span class="math notranslate nohighlight">\((y - 2) ^ 2= 0\)</span>, so <span class="math notranslate nohighlight">\(y - 2= 0\)</span>, and so <span class="math notranslate nohighlight">\(y = 2\)</span>.</p>
</div>
<p>In Lean, the result of <a class="reference internal" href="02_Proofs_with_Structure.html#prove-sq-le-sq"><span class="std std-numref">Example 2.1.7</span></a> is available as the lemma <code class="docutils literal notranslate"><span class="pre">sq_le_sq'</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="bp">&#8707;!</span> <span class="n">x</span> <span class="o">:</span> <span class="n">&#8474;</span><span class="o">,</span> <span class="bp">&#8704;</span> <span class="n">a</span><span class="o">,</span> <span class="n">a</span> <span class="bp">&#8805;</span> <span class="mi">1</span> <span class="bp">&#8594;</span> <span class="n">a</span> <span class="bp">&#8804;</span> <span class="mi">3</span> <span class="bp">&#8594;</span> <span class="o">(</span><span class="n">a</span> <span class="bp">-</span> <span class="n">x</span><span class="o">)</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">&#8804;</span> <span class="mi">1</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</section>
<section id="id24">
<h3><span class="section-number">4.3.3. </span>Example<a class="headerlink" href="#id24" title="Permalink to this headline">&#61633;</a></h3>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Let <span class="math notranslate nohighlight">\(x\)</span> be a rational number, and suppose that there exists a unique rational number
<span class="math notranslate nohighlight">\(a\)</span> such that <span class="math notranslate nohighlight">\(a^2=x\)</span>.  Show that <span class="math notranslate nohighlight">\(x=0\)</span>.</p>
</div>
<p>More colloquially: the only rational number with a unique square root is 0.</p>
<div class="admonition-solution admonition">
<p class="admonition-title">Solution</p>
<p>We first show that <span class="math notranslate nohighlight">\(-a=a\)</span>.  Indeed,</p>
<div class="math notranslate nohighlight">
\[\begin{split}(-a)^2&amp;=a^2\\
&amp;=x,\end{split}\]</div>
<p>and since <span class="math notranslate nohighlight">\(a\)</span> is the unique rational number such that <span class="math notranslate nohighlight">\(a^2=x\)</span>, this means that
<span class="math notranslate nohighlight">\(-a=a\)</span>.</p>
<p>It follows that</p>
<div class="math notranslate nohighlight">
\[\begin{split}a &amp;= \frac{a - (-a)}{ 2}\\
&amp;=\frac{a-a}{2}\\
&amp; = 0.\end{split}\]</div>
<p>So <span class="math notranslate nohighlight">\(x=0\)</span> also:</p>
<div class="math notranslate nohighlight">
\[\begin{split}x &amp;= a ^ 2 \\
&amp;= 0 ^ 2\\
&amp; = 0.\end{split}\]</div>
</div>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">{</span><span class="n">x</span> <span class="o">:</span> <span class="n">&#8474;</span><span class="o">}</span> <span class="o">(</span><span class="n">hx</span> <span class="o">:</span> <span class="bp">&#8707;!</span> <span class="n">a</span> <span class="o">:</span> <span class="n">&#8474;</span><span class="o">,</span> <span class="n">a</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">=</span> <span class="n">x</span><span class="o">)</span> <span class="o">:</span> <span class="n">x</span> <span class="bp">=</span> <span class="mi">0</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">obtain</span> <span class="o">&#10216;</span><span class="n">a</span><span class="o">,</span> <span class="n">ha1</span><span class="o">,</span> <span class="n">ha2</span><span class="o">&#10217;</span> <span class="o">:=</span> <span class="n">hx</span>
  <span class="k">have</span> <span class="n">h1</span> <span class="o">:</span> <span class="bp">-</span><span class="n">a</span> <span class="bp">=</span> <span class="n">a</span>
  <span class="bp">&#183;</span> <span class="n">apply</span> <span class="n">ha2</span>
    <span class="k">calc</span>
      <span class="o">(</span><span class="bp">-</span><span class="n">a</span><span class="o">)</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">=</span> <span class="n">a</span> <span class="bp">^</span> <span class="mi">2</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">ring</span>
      <span class="n">_</span> <span class="bp">=</span> <span class="n">x</span> <span class="o">:=</span> <span class="n">ha1</span>
  <span class="k">have</span> <span class="n">h2</span> <span class="o">:=</span>
    <span class="k">calc</span>
      <span class="n">a</span> <span class="bp">=</span> <span class="o">(</span><span class="n">a</span> <span class="bp">-</span> <span class="bp">-</span><span class="n">a</span><span class="o">)</span> <span class="bp">/</span> <span class="mi">2</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">ring</span>
      <span class="n">_</span> <span class="bp">=</span> <span class="o">(</span><span class="n">a</span> <span class="bp">-</span> <span class="n">a</span><span class="o">)</span> <span class="bp">/</span> <span class="mi">2</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">rw</span> <span class="o">[</span><span class="n">h1</span><span class="o">]</span>
      <span class="n">_</span> <span class="bp">=</span> <span class="mi">0</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">ring</span>
  <span class="k">calc</span>
    <span class="n">x</span> <span class="bp">=</span> <span class="n">a</span> <span class="bp">^</span> <span class="mi">2</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">rw</span> <span class="o">[</span><span class="n">ha1</span><span class="o">]</span>
    <span class="n">_</span> <span class="bp">=</span> <span class="mi">0</span> <span class="bp">^</span> <span class="mi">2</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">rw</span> <span class="o">[</span><span class="n">h2</span><span class="o">]</span>
    <span class="n">_</span> <span class="bp">=</span> <span class="mi">0</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">ring</span>
</pre></div>
</div>
</section>
<section id="division-algorithm">
<span id="id25"></span><h3><span class="section-number">4.3.4. </span>Example<a class="headerlink" href="#division-algorithm" title="Permalink to this headline">&#61633;</a></h3>
<p>The following is an important theorem about the integers, which we will prove later in the book, in
the exercises to <a class="reference internal" href="06_Induction.html#constructive-division-algorithm"><span class="std std-numref">Section 6.6</span></a>.</p>
<div class="admonition-theorem-the-division-algorithm admonition">
<p class="admonition-title">Theorem (the Division Algorithm)</p>
<p>Let <span class="math notranslate nohighlight">\(a\)</span> and <span class="math notranslate nohighlight">\(b\)</span> be integers, with <span class="math notranslate nohighlight">\(b\)</span> positive.  Then there exists a unique
integer <span class="math notranslate nohighlight">\(r\)</span> between 0 (inclusive) and <span class="math notranslate nohighlight">\(b\)</span> (exclusive), such that
<span class="math notranslate nohighlight">\(a\equiv r\mod b\)</span>.</p>
</div>
<p>This lemma is what allows us to do case divisions according to congruence class modulo <span class="math notranslate nohighlight">\(b\)</span>
(the Lean tactic <code class="docutils literal notranslate"><span class="pre">mod_cases</span></code>).  But it&#8217;s actually a bit more powerful, since the &#8220;uniqueness&#8221; part
of the statement provides extra information.</p>
<p>In the Lean library it is available in the following form:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">lemma</span> <span class="n">Int.existsUnique_modEq_lt</span> <span class="o">(</span><span class="n">a</span> <span class="n">b</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">)</span> <span class="o">(</span><span class="n">h</span> <span class="o">:</span> <span class="mi">0</span> <span class="bp">&lt;</span> <span class="n">b</span><span class="o">)</span> <span class="o">:</span>
  <span class="bp">&#8707;!</span> <span class="n">r</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">,</span> <span class="mi">0</span> <span class="bp">&#8804;</span> <span class="n">r</span> <span class="bp">&#8743;</span> <span class="n">r</span> <span class="bp">&lt;</span> <span class="n">b</span> <span class="bp">&#8743;</span> <span class="n">a</span> <span class="bp">&#8801;</span> <span class="n">r</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="n">b</span><span class="o">]</span> <span class="o">:=</span>
</pre></div>
</div>
<p>To understand this theorem better, let&#8217;s prove just one of the infinitely many cases of this
theorem.</p>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Show that there exists a unique integer <span class="math notranslate nohighlight">\(r\)</span>, such that <span class="math notranslate nohighlight">\(0\le r &lt; 5\)</span> and
<span class="math notranslate nohighlight">\(14\equiv r\mod 5\)</span>.</p>
</div>
<div class="admonition-solution admonition">
<p class="admonition-title">Solution</p>
<p>We will show that the unique integer with this property is 4.</p>
<p>First, we show that 4 has this property.  It is true that <span class="math notranslate nohighlight">\(0\le 4 &lt; 5\)</span>, and since
<span class="math notranslate nohighlight">\(14 - 4 = 5 \cdot 2\)</span> it is true that <span class="math notranslate nohighlight">\(14\equiv r\mod 5\)</span>.</p>
<p>Now, let <span class="math notranslate nohighlight">\(r\)</span> be an integer for which <span class="math notranslate nohighlight">\(0\le r &lt; 5\)</span> and <span class="math notranslate nohighlight">\(14\equiv r\mod 5\)</span>.  Then
there exists an integer <span class="math notranslate nohighlight">\(q\)</span> such that <span class="math notranslate nohighlight">\(14-r=5q\)</span>.</p>
<p>We have,</p>
<div class="math notranslate nohighlight">
\[\begin{split}5&amp; \cdot 1 &lt; 14 - r \\
&amp; = 5q,\end{split}\]</div>
<p>so since <span class="math notranslate nohighlight">\(5\)</span> is positive, <span class="math notranslate nohighlight">\(1&lt;q\)</span>.  Similarly, we have</p>
<div class="math notranslate nohighlight">
\[\begin{split}5 q &amp;= 14 - r \\
  &amp; &lt; 5 \cdot 3\end{split}\]</div>
<p>and so since <span class="math notranslate nohighlight">\(5\)</span> is positive, <span class="math notranslate nohighlight">\(q&lt;3\)</span>.</p>
<p>Therefore <span class="math notranslate nohighlight">\(q\)</span> must be 2, the only integer
strictly between 1 and 3.  So <span class="math notranslate nohighlight">\(r=14-5\cdot 2=4\)</span>.</p>
</div>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="bp">&#8707;!</span> <span class="n">r</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">,</span> <span class="mi">0</span> <span class="bp">&#8804;</span> <span class="n">r</span> <span class="bp">&#8743;</span> <span class="n">r</span> <span class="bp">&lt;</span> <span class="mi">5</span> <span class="bp">&#8743;</span> <span class="mi">14</span> <span class="bp">&#8801;</span> <span class="n">r</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="mi">5</span><span class="o">]</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">use</span> <span class="mi">4</span>
  <span class="n">dsimp</span>
  <span class="n">constructor</span>
  <span class="bp">&#183;</span> <span class="n">constructor</span>
    <span class="bp">&#183;</span> <span class="n">numbers</span>
    <span class="n">constructor</span>
    <span class="bp">&#183;</span> <span class="n">numbers</span>
    <span class="n">use</span> <span class="mi">2</span>
    <span class="n">numbers</span>
  <span class="n">intro</span> <span class="n">r</span> <span class="n">hr</span>
  <span class="n">obtain</span> <span class="o">&#10216;</span><span class="n">hr1</span><span class="o">,</span> <span class="n">hr2</span><span class="o">,</span> <span class="n">q</span><span class="o">,</span> <span class="n">hr3</span><span class="o">&#10217;</span> <span class="o">:=</span> <span class="n">hr</span>
  <span class="k">have</span> <span class="o">:=</span>
    <span class="k">calc</span>
      <span class="mi">5</span> <span class="bp">*</span> <span class="mi">1</span> <span class="bp">&lt;</span> <span class="mi">14</span> <span class="bp">-</span> <span class="n">r</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">addarith</span> <span class="o">[</span><span class="n">hr2</span><span class="o">]</span>
      <span class="n">_</span> <span class="bp">=</span> <span class="mi">5</span> <span class="bp">*</span> <span class="n">q</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">rw</span> <span class="o">[</span><span class="n">hr3</span><span class="o">]</span>
  <span class="n">cancel</span> <span class="mi">5</span> <span class="n">at</span> <span class="n">this</span>
  <span class="k">have</span> <span class="o">:=</span>
    <span class="k">calc</span>
      <span class="mi">5</span> <span class="bp">*</span> <span class="n">q</span> <span class="bp">=</span> <span class="mi">14</span> <span class="bp">-</span> <span class="n">r</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">rw</span> <span class="o">[</span><span class="n">hr3</span><span class="o">]</span>
      <span class="n">_</span> <span class="bp">&lt;</span> <span class="mi">5</span> <span class="bp">*</span> <span class="mi">3</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">addarith</span> <span class="o">[</span><span class="n">hr1</span><span class="o">]</span>
  <span class="n">cancel</span> <span class="mi">5</span> <span class="n">at</span> <span class="n">this</span>
  <span class="n">interval_cases</span> <span class="n">q</span>
  <span class="n">addarith</span> <span class="o">[</span><span class="n">hr3</span><span class="o">]</span>
</pre></div>
</div>
</section>
<section id="id26">
<h3><span class="section-number">4.3.5. </span>Exercises<a class="headerlink" href="#id26" title="Permalink to this headline">&#61633;</a></h3>
<ol class="arabic">
<li><p>Show that there exists a unique rational number <span class="math notranslate nohighlight">\(x\)</span>, such that <span class="math notranslate nohighlight">\(4x-3=9\)</span>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="bp">&#8707;!</span> <span class="n">x</span> <span class="o">:</span> <span class="n">&#8474;</span><span class="o">,</span> <span class="mi">4</span> <span class="bp">*</span> <span class="n">x</span> <span class="bp">-</span> <span class="mi">3</span> <span class="bp">=</span> <span class="mi">9</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Show that there exists a unique natural number <span class="math notranslate nohighlight">\(n\)</span>, such that for all natural numbers
<span class="math notranslate nohighlight">\(a\)</span>, we have <span class="math notranslate nohighlight">\(n\le a\)</span>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="bp">&#8707;!</span> <span class="n">n</span> <span class="o">:</span> <span class="n">&#8469;</span><span class="o">,</span> <span class="bp">&#8704;</span> <span class="n">a</span><span class="o">,</span> <span class="n">n</span> <span class="bp">&#8804;</span> <span class="n">a</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Show that there exists a unique integer <span class="math notranslate nohighlight">\(r\)</span>, such that <span class="math notranslate nohighlight">\(0\le r &lt; 3\)</span> and
<span class="math notranslate nohighlight">\(11\equiv r\mod 3\)</span>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="bp">&#8707;!</span> <span class="n">r</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">,</span> <span class="mi">0</span> <span class="bp">&#8804;</span> <span class="n">r</span> <span class="bp">&#8743;</span> <span class="n">r</span> <span class="bp">&lt;</span> <span class="mi">3</span> <span class="bp">&#8743;</span> <span class="mi">11</span> <span class="bp">&#8801;</span> <span class="n">r</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="mi">3</span><span class="o">]</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
</ol>
</section>
</section>
<section id="contradictory-hypotheses">
<span id="contradiction-hyp"></span><h2><span class="section-number">4.4. </span>Contradictory hypotheses<a class="headerlink" href="#contradictory-hypotheses" title="Permalink to this headline">&#61633;</a></h2>
<section id="pos-of-mul-pos-right-proof">
<span id="id27"></span><h3><span class="section-number">4.4.1. </span>Example<a class="headerlink" href="#pos-of-mul-pos-right-proof" title="Permalink to this headline">&#61633;</a></h3>
<p>Sometimes, we encounter a situation with two contradictory hypotheses.  At this point, there is no
need to prove anything more.  Two contradictory hypotheses mean that the situation we had
hypothesized can&#8217;t actually happen.</p>
<p>It is quite common to encounter this when giving a proof by cases.  You might reduce the problem to
some list of cases, prove your goal in some of those cases, and prove that the other cases are
impossible.</p>
<p>Here is an example of this kind of reasoning.  I have written the solution very pedantically, to
make the point clearer.</p>
<div class="admonition-lemma admonition">
<p class="admonition-title">Lemma</p>
<p>Let <span class="math notranslate nohighlight">\(x\)</span> and <span class="math notranslate nohighlight">\(y\)</span> be real numbers, and suppose that <span class="math notranslate nohighlight">\(0&lt;xy\)</span> and <span class="math notranslate nohighlight">\(0 \le x\)</span>.
Show that <span class="math notranslate nohighlight">\(0&lt;y\)</span>.</p>
</div>
<p>We have used this fact many times before &#8211; it is one of the facts which underlie the <code class="docutils literal notranslate"><span class="pre">cancel</span></code>
tactic.</p>
<div class="admonition-proof admonition">
<p class="admonition-title">Proof</p>
<p>We consider two cases, depending on whether or not <span class="math notranslate nohighlight">\(y\)</span> is positive.</p>
<p><strong>Case 1</strong> (<span class="math notranslate nohighlight">\(y \le 0\)</span>): Since <span class="math notranslate nohighlight">\(0 \le x\)</span>, we have that</p>
<div class="math notranslate nohighlight">
\[\begin{split}0 &amp;= x \cdot 0\\
&amp;\geq xy,\end{split}\]</div>
<p>and so it is false that <span class="math notranslate nohighlight">\(0&lt;xy\)</span>. This contradicts the hypothesis that <span class="math notranslate nohighlight">\(0&lt; xy\)</span>, so this
case can&#8217;t happen.</p>
<p><strong>Case 2</strong> (<span class="math notranslate nohighlight">\(0 &lt; y\)</span>): This is what we needed to prove, so we are done.</p>
</div>
<p>In Lean, the tactic <code class="docutils literal notranslate"><span class="pre">contradiction</span></code> concludes a (part of a) proof by pointing out two
contradictory hypotheses.  In the Lean translation of this example, notice that right before it&#8217;s
used, the goal state is</p>
<div class="highlight-text notranslate"><div class="highlight"><pre><span></span>y x : &#8477;
h : 0 &lt; x * y
hx : 0 &#8804; x
hneg : y &#8804; 0
this : &#172;0 &lt; x * y
&#8866; 0 &lt; y
</pre></div>
</div>
<p>which contains the contradictory hypotheses <code class="docutils literal notranslate"><span class="pre">h</span> <span class="pre">:</span> <span class="pre">0</span> <span class="pre">&lt;</span> <span class="pre">x</span> <span class="pre">*</span> <span class="pre">y</span></code> and <code class="docutils literal notranslate"><span class="pre">this</span> <span class="pre">:</span> <span class="pre">&#172;0</span> <span class="pre">&lt;</span> <span class="pre">x</span> <span class="pre">*</span> <span class="pre">y</span></code>.  (Remember
that <code class="docutils literal notranslate"><span class="pre">&#172;</span></code> is the logical symbol for &#8220;not&#8221;.  If you don&#8217;t name a hypothesis, Lean labels it
<code class="docutils literal notranslate"><span class="pre">this</span></code>.)</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">{</span><span class="n">y</span> <span class="o">:</span> <span class="n">&#8477;</span><span class="o">}</span> <span class="o">(</span><span class="n">x</span> <span class="o">:</span> <span class="n">&#8477;</span><span class="o">)</span> <span class="o">(</span><span class="n">h</span> <span class="o">:</span> <span class="mi">0</span> <span class="bp">&lt;</span> <span class="n">x</span> <span class="bp">*</span> <span class="n">y</span><span class="o">)</span> <span class="o">(</span><span class="n">hx</span> <span class="o">:</span> <span class="mi">0</span> <span class="bp">&#8804;</span> <span class="n">x</span><span class="o">)</span> <span class="o">:</span> <span class="mi">0</span> <span class="bp">&lt;</span> <span class="n">y</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">obtain</span> <span class="n">hneg</span> <span class="bp">|</span> <span class="n">hpos</span> <span class="o">:</span> <span class="n">y</span> <span class="bp">&#8804;</span> <span class="mi">0</span> <span class="bp">&#8744;</span> <span class="mi">0</span> <span class="bp">&lt;</span> <span class="n">y</span> <span class="o">:=</span> <span class="n">le_or_lt</span> <span class="n">y</span> <span class="mi">0</span>
  <span class="bp">&#183;</span> <span class="c1">-- the case `y &#8804; 0`</span>
    <span class="k">have</span> <span class="o">:</span> <span class="bp">&#172;</span><span class="mi">0</span> <span class="bp">&lt;</span> <span class="n">x</span> <span class="bp">*</span> <span class="n">y</span>
    <span class="bp">&#183;</span> <span class="n">apply</span> <span class="n">not_lt_of_ge</span>
      <span class="k">calc</span>
        <span class="mi">0</span> <span class="bp">=</span> <span class="n">x</span> <span class="bp">*</span> <span class="mi">0</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">ring</span>
        <span class="n">_</span> <span class="bp">&#8805;</span> <span class="n">x</span> <span class="bp">*</span> <span class="n">y</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">rel</span> <span class="o">[</span><span class="n">hneg</span><span class="o">]</span>
    <span class="n">contradiction</span>
  <span class="bp">&#183;</span> <span class="c1">-- the case `0 &lt; y`</span>
    <span class="n">apply</span> <span class="n">hpos</span>
</pre></div>
</div>
</section>
<section id="numbers-contradiction">
<span id="id28"></span><h3><span class="section-number">4.4.2. </span>Example<a class="headerlink" href="#numbers-contradiction" title="Permalink to this headline">&#61633;</a></h3>
<p>One very common way to get a contradiction is by proving that the hypotheses imply some &#8220;obviously
false&#8221; numeric fact, whose falseness can be checked with <code class="docutils literal notranslate"><span class="pre">numbers</span></code>.</p>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Let <span class="math notranslate nohighlight">\(t\)</span> be an integer which is less than 3, and suppose that <span class="math notranslate nohighlight">\(t - 1 = 6\)</span>.  Show that
<span class="math notranslate nohighlight">\(t=13\)</span>.</p>
</div>
<div class="admonition-solution admonition">
<p class="admonition-title">Solution</p>
<p>We have,</p>
<div class="math notranslate nohighlight">
\[\begin{split}7 &amp;= t\\
&amp;&lt;3.\end{split}\]</div>
<p>But clearly it&#8217;s false that <span class="math notranslate nohighlight">\(7 &lt;3\)</span>, contradiction.  So any conclusion (including
<span class="math notranslate nohighlight">\(t=13\)</span>) is true.</p>
</div>
<p>You can write this proof up in Lean directly using the <code class="docutils literal notranslate"><span class="pre">contradiction</span></code> tactic, as in the previous
examples:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">{</span><span class="n">t</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">}</span> <span class="o">(</span><span class="n">h2</span> <span class="o">:</span> <span class="n">t</span> <span class="bp">&lt;</span> <span class="mi">3</span><span class="o">)</span> <span class="o">(</span><span class="n">h</span> <span class="o">:</span> <span class="n">t</span> <span class="bp">-</span> <span class="mi">1</span> <span class="bp">=</span> <span class="mi">6</span><span class="o">)</span> <span class="o">:</span> <span class="n">t</span> <span class="bp">=</span> <span class="mi">13</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="k">have</span> <span class="n">H</span> <span class="o">:=</span>
  <span class="k">calc</span>
    <span class="mi">7</span> <span class="bp">=</span> <span class="n">t</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">addarith</span> <span class="o">[</span><span class="n">h</span><span class="o">]</span>
    <span class="n">_</span> <span class="bp">&lt;</span> <span class="mi">3</span> <span class="o">:=</span> <span class="n">h2</span>
  <span class="k">have</span> <span class="o">:</span> <span class="bp">&#172;</span><span class="o">(</span><span class="mi">7</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">)</span> <span class="bp">&lt;</span> <span class="mi">3</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">numbers</span>
  <span class="n">contradiction</span>
</pre></div>
</div>
<p>But the pattern is also sufficiently common that there is a shorthand in Lean.  If <code class="docutils literal notranslate"><span class="pre">H</span></code> is a
hypothesis whose negation can be proved by <code class="docutils literal notranslate"><span class="pre">numbers</span></code>, then writing <code class="docutils literal notranslate"><span class="pre">numbers</span> <span class="pre">at</span> <span class="pre">H</span></code> will
close the goal.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">{</span><span class="n">t</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">}</span> <span class="o">(</span><span class="n">h2</span> <span class="o">:</span> <span class="n">t</span> <span class="bp">&lt;</span> <span class="mi">3</span><span class="o">)</span> <span class="o">(</span><span class="n">h</span> <span class="o">:</span> <span class="n">t</span> <span class="bp">-</span> <span class="mi">1</span> <span class="bp">=</span> <span class="mi">6</span><span class="o">)</span> <span class="o">:</span> <span class="n">t</span> <span class="bp">=</span> <span class="mi">13</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="k">have</span> <span class="n">H</span> <span class="o">:=</span>
  <span class="k">calc</span>
    <span class="mi">7</span> <span class="bp">=</span> <span class="n">t</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">addarith</span> <span class="o">[</span><span class="n">h</span><span class="o">]</span>
    <span class="n">_</span> <span class="bp">&lt;</span> <span class="mi">3</span> <span class="o">:=</span> <span class="n">h2</span>
  <span class="n">numbers</span> <span class="n">at</span> <span class="n">H</span> <span class="c1">-- this is a contradiction!</span>
</pre></div>
</div>
</section>
<section id="mod-contradictory">
<span id="id29"></span><h3><span class="section-number">4.4.3. </span>Example<a class="headerlink" href="#mod-contradictory" title="Permalink to this headline">&#61633;</a></h3>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Show that if <span class="math notranslate nohighlight">\(n^2+n+1\equiv 1\mod 3\)</span> then <span class="math notranslate nohighlight">\(n\equiv 0\mod 3\)</span> or
<span class="math notranslate nohighlight">\(n\equiv 2\mod 3\)</span>.</p>
</div>
<div class="admonition-solution admonition">
<p class="admonition-title">Solution</p>
<p>We consider cases according to the residue of <span class="math notranslate nohighlight">\(n\)</span> modulo 3.  If <span class="math notranslate nohighlight">\(n\equiv 0\mod 3\)</span> or
<span class="math notranslate nohighlight">\(n\equiv 2\mod 3\)</span>, then we are done.  Otherwise, <span class="math notranslate nohighlight">\(n\equiv 1\mod 3\)</span>, so</p>
<div class="math notranslate nohighlight">
\[\begin{split}0 &amp;\equiv 0 + 3 \cdot 1 \mod 3 \\
  &amp; = 1 ^ 2 + 1 + 1\\
  &amp;\equiv n ^ 2 + n + 1 \mod 3\\
  &amp;\equiv 1 \mod 3,\end{split}\]</div>
<p>contradiction.</p>
</div>
<p>Notice that in the above proof we did some extra work to get <span class="math notranslate nohighlight">\(0\equiv 1\mod 3\)</span> for the
contradiction, rather than <span class="math notranslate nohighlight">\(3\equiv 1\mod 3\)</span>, which could have been obtained more easily:</p>
<div class="math notranslate nohighlight">
\[\begin{split}3 &amp; = 1 ^ 2 + 1 + 1\\
  &amp;\equiv \ldots\end{split}\]</div>
<p>For the purposes of this book, we will treat as &#8220;obviously true/false&#8221; only congruences
<span class="math notranslate nohighlight">\(i\equiv j\mod n\)</span> for which <span class="math notranslate nohighlight">\(0 \le i&lt;n\)</span> and <span class="math notranslate nohighlight">\(0 \le j&lt;n\)</span>.  We will ask that
congruences involving larger numbers be explicitly reduced modulo <span class="math notranslate nohighlight">\(n\)</span>, as we did here in
reducing <span class="math notranslate nohighlight">\(3=1 ^ 2 + 1 + 1\)</span> to <span class="math notranslate nohighlight">\(0 + 3 \cdot 1\)</span> modulo 3 and thus to <span class="math notranslate nohighlight">\(0\)</span>.</p>
<p>The mathematical justification for this is the uniqueness lemma <code class="docutils literal notranslate"><span class="pre">Int.existsUnique_modEq_lt</span></code>,
discussed in <a class="reference internal" href="#division-algorithm"><span class="std std-numref">Example 4.3.4</span></a>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">(</span><span class="n">n</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">)</span> <span class="o">(</span><span class="n">hn</span> <span class="o">:</span> <span class="n">n</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">+</span> <span class="n">n</span> <span class="bp">+</span> <span class="mi">1</span> <span class="bp">&#8801;</span> <span class="mi">1</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="mi">3</span><span class="o">])</span> <span class="o">:</span>
    <span class="n">n</span> <span class="bp">&#8801;</span> <span class="mi">0</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="mi">3</span><span class="o">]</span> <span class="bp">&#8744;</span> <span class="n">n</span> <span class="bp">&#8801;</span> <span class="mi">2</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="mi">3</span><span class="o">]</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">mod_cases</span> <span class="n">h</span> <span class="o">:</span> <span class="n">n</span> <span class="bp">%</span> <span class="mi">3</span>
  <span class="bp">&#183;</span> <span class="c1">-- case 1: `n &#8801; 0 [ZMOD 3]`</span>
    <span class="n">left</span>
    <span class="n">apply</span> <span class="n">h</span>
  <span class="bp">&#183;</span> <span class="c1">-- case 2: `n &#8801; 1 [ZMOD 3]`</span>
    <span class="k">have</span> <span class="n">H</span> <span class="o">:=</span>
      <span class="k">calc</span> <span class="mi">0</span> <span class="bp">&#8801;</span> <span class="mi">0</span> <span class="bp">+</span> <span class="mi">3</span> <span class="bp">*</span> <span class="mi">1</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="mi">3</span><span class="o">]</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">extra</span>
      <span class="n">_</span> <span class="bp">=</span> <span class="mi">1</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">+</span> <span class="mi">1</span> <span class="bp">+</span> <span class="mi">1</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">numbers</span>
      <span class="n">_</span> <span class="bp">&#8801;</span> <span class="n">n</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">+</span> <span class="n">n</span> <span class="bp">+</span> <span class="mi">1</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="mi">3</span><span class="o">]</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">rel</span> <span class="o">[</span><span class="n">h</span><span class="o">]</span>
      <span class="n">_</span> <span class="bp">&#8801;</span> <span class="mi">1</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="mi">3</span><span class="o">]</span> <span class="o">:=</span> <span class="n">hn</span>
    <span class="n">numbers</span> <span class="n">at</span> <span class="n">H</span> <span class="c1">-- contradiction!</span>
  <span class="bp">&#183;</span> <span class="c1">-- case 3: `n &#8801; 2 [ZMOD 3]`</span>
    <span class="n">right</span>
    <span class="n">apply</span> <span class="n">h</span>
</pre></div>
</div>
</section>
<section id="prime-test">
<span id="id30"></span><h3><span class="section-number">4.4.4. </span>Example<a class="headerlink" href="#prime-test" title="Permalink to this headline">&#61633;</a></h3>
<p>We defined prime numbers in <a class="reference internal" href="#prime-def"><span class="std std-numref">Example 4.1.8</span></a>, and proved that 2 was prime. Let&#8217;s now
prove a slight reformulation of the definition, which will be convenient in showing that other
numbers are prime.</p>
<div class="admonition-lemma admonition">
<p class="admonition-title">Lemma</p>
<p>Let <span class="math notranslate nohighlight">\(p\)</span> be a natural number greater than or equal to 2.  Suppose that for all natural
numbers <span class="math notranslate nohighlight">\(m\)</span> for which <span class="math notranslate nohighlight">\(1&lt;m&lt;p\)</span>, it is not true that <span class="math notranslate nohighlight">\(m\)</span> is a factor of <span class="math notranslate nohighlight">\(p\)</span>.
Show that <span class="math notranslate nohighlight">\(p\)</span> is prime.</p>
</div>
<div class="admonition-proof admonition">
<p class="admonition-title">Proof</p>
<p>Since we are given that <span class="math notranslate nohighlight">\(2 \le p\)</span>, what&#8217;s left is to prove the second part of the definition
&#8220;prime&#8221;: let <span class="math notranslate nohighlight">\(m\)</span> be a factor of <span class="math notranslate nohighlight">\(p\)</span> (<span class="math notranslate nohighlight">\(\star\)</span>); we must show that <span class="math notranslate nohighlight">\(m=1\)</span> or
<span class="math notranslate nohighlight">\(m=p\)</span>.</p>
<p>Since <span class="math notranslate nohighlight">\(m\)</span> is a factor of <span class="math notranslate nohighlight">\(p\)</span>, we have that <span class="math notranslate nohighlight">\(1 \le m\)</span>. So either <span class="math notranslate nohighlight">\(m=1\)</span> or
<span class="math notranslate nohighlight">\(1&lt;m\)</span>; we consider cases accordingly.</p>
<p><strong>Case 1</strong> (<span class="math notranslate nohighlight">\(m=1\)</span>): This immediately gives our goal that <span class="math notranslate nohighlight">\(m=1\)</span> or <span class="math notranslate nohighlight">\(m=p\)</span>.</p>
<p><strong>Case 2</strong> (<span class="math notranslate nohighlight">\(1&lt;m\)</span>):  Since <span class="math notranslate nohighlight">\(m\)</span> is a factor of <span class="math notranslate nohighlight">\(p\)</span>, we have that
<span class="math notranslate nohighlight">\(m \le p\)</span>. So either <span class="math notranslate nohighlight">\(m=p\)</span> or <span class="math notranslate nohighlight">\(m&lt;p\)</span>; we consider cases accordingly.</p>
<p><strong>Case 2(i)</strong> (<span class="math notranslate nohighlight">\(m=p\)</span>):  This immediately gives our goal that <span class="math notranslate nohighlight">\(m=1\)</span> or <span class="math notranslate nohighlight">\(m=p\)</span>.</p>
<p><strong>Case 2(ii)</strong> (<span class="math notranslate nohighlight">\(m&lt;p\)</span>):  We have now established that <span class="math notranslate nohighlight">\(1&lt;m&lt;p\)</span>, and by one of the
facts given in the problem statement, this means that <span class="math notranslate nohighlight">\(m\)</span> is not a factor of <span class="math notranslate nohighlight">\(p\)</span>.
This contradicts the earlier statement (<span class="math notranslate nohighlight">\(\star\)</span>).</p>
</div>
<p>I&#8217;ve filled in about half of this proof in Lean; fill in the rest, including the final
contradiction.  If you need to look up the Lean names for the size bounds on factors, they were
proved in <a class="reference internal" href="03_Parity_and_Divisibility.html#dvd-bd-1"><span class="std std-numref">Example 3.2.7</span></a> and <a class="reference internal" href="03_Parity_and_Divisibility.html#dvd-bd-2"><span class="std std-numref">Example 3.2.8</span></a>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">{</span><span class="n">p</span> <span class="o">:</span> <span class="n">&#8469;</span><span class="o">}</span> <span class="o">(</span><span class="n">hp</span> <span class="o">:</span> <span class="mi">2</span> <span class="bp">&#8804;</span> <span class="n">p</span><span class="o">)</span> <span class="o">(</span><span class="n">H</span> <span class="o">:</span> <span class="bp">&#8704;</span> <span class="n">m</span> <span class="o">:</span> <span class="n">&#8469;</span><span class="o">,</span> <span class="mi">1</span> <span class="bp">&lt;</span> <span class="n">m</span> <span class="bp">&#8594;</span> <span class="n">m</span> <span class="bp">&lt;</span> <span class="n">p</span> <span class="bp">&#8594;</span> <span class="bp">&#172;</span><span class="n">m</span> <span class="bp">&#8739;</span> <span class="n">p</span><span class="o">)</span> <span class="o">:</span> <span class="n">Prime</span> <span class="n">p</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">constructor</span>
  <span class="bp">&#183;</span> <span class="n">apply</span> <span class="n">hp</span> <span class="c1">-- show that `2 &#8804; p`</span>
  <span class="n">intro</span> <span class="n">m</span> <span class="n">hmp</span>
  <span class="k">have</span> <span class="n">hp&#39;</span> <span class="o">:</span> <span class="mi">0</span> <span class="bp">&lt;</span> <span class="n">p</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">extra</span>
  <span class="k">have</span> <span class="n">h1m</span> <span class="o">:</span> <span class="mi">1</span> <span class="bp">&#8804;</span> <span class="n">m</span> <span class="o">:=</span> <span class="n">Nat.pos_of_dvd_of_pos</span> <span class="n">hmp</span> <span class="n">hp&#39;</span>
  <span class="n">obtain</span> <span class="n">hm</span> <span class="bp">|</span> <span class="n">hm_left</span> <span class="o">:</span> <span class="mi">1</span> <span class="bp">=</span> <span class="n">m</span> <span class="bp">&#8744;</span> <span class="mi">1</span> <span class="bp">&lt;</span> <span class="n">m</span> <span class="o">:=</span> <span class="n">eq_or_lt_of_le</span> <span class="n">h1m</span>
  <span class="bp">&#183;</span> <span class="c1">-- the case `m = 1`</span>
    <span class="n">left</span>
    <span class="n">addarith</span> <span class="o">[</span><span class="n">hm</span><span class="o">]</span>
  <span class="c1">-- the case `1 &lt; m`</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
<p>We record this for future use under the Lean name <code class="docutils literal notranslate"><span class="pre">prime_test</span></code>.</p>
<p>Here&#8217;s an example of how this prime-testing lemma is used.</p>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Show that 5 is prime.</p>
</div>
<div class="admonition-solution admonition">
<p class="admonition-title">Solution</p>
<p>Clearly <span class="math notranslate nohighlight">\(2 &#8804; 5\)</span>.  Let <span class="math notranslate nohighlight">\(m\)</span> be a natural number with <span class="math notranslate nohighlight">\(1&lt;m&lt;5\)</span>.  We must show that
5 is not a multiple of <span class="math notranslate nohighlight">\(m\)</span>. There are three cases to check:</p>
<p><strong>Case 1</strong> (<span class="math notranslate nohighlight">\(m=2\)</span>):  Since 5 lies between the consecutive multiples
<span class="math notranslate nohighlight">\(2\cdot 2\)</span> and <span class="math notranslate nohighlight">\(2 \cdot 3\)</span> of 2, it is not a multiple of 2.</p>
<p><strong>Case 2</strong> (<span class="math notranslate nohighlight">\(m=3\)</span>):  Since 5 lies between the consecutive multiples
<span class="math notranslate nohighlight">\(3\cdot 1\)</span> and <span class="math notranslate nohighlight">\(3 \cdot 2\)</span> of 3, it is not a multiple of 3.</p>
<p><strong>Case 3</strong> (<span class="math notranslate nohighlight">\(m=4\)</span>):  Since 5 lies between the consecutive multiples
<span class="math notranslate nohighlight">\(4\cdot 1\)</span> and <span class="math notranslate nohighlight">\(4 \cdot 2\)</span> of 4, it is not a multiple of 4.</p>
</div>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="n">Prime</span> <span class="mi">5</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">apply</span> <span class="n">prime_test</span>
  <span class="bp">&#183;</span> <span class="n">numbers</span>
  <span class="n">intro</span> <span class="n">m</span> <span class="n">hm_left</span> <span class="n">hm_right</span>
  <span class="n">apply</span> <span class="n">Nat.not_dvd_of_exists_lt_and_lt</span>
  <span class="n">interval_cases</span> <span class="n">m</span>
  <span class="bp">&#183;</span> <span class="n">use</span> <span class="mi">2</span>
    <span class="n">constructor</span> <span class="bp">&lt;;&gt;</span> <span class="n">numbers</span>
  <span class="bp">&#183;</span> <span class="n">use</span> <span class="mi">1</span>
    <span class="n">constructor</span> <span class="bp">&lt;;&gt;</span> <span class="n">numbers</span>
  <span class="bp">&#183;</span> <span class="n">use</span> <span class="mi">1</span>
    <span class="n">constructor</span> <span class="bp">&lt;;&gt;</span> <span class="n">numbers</span>
</pre></div>
</div>
<p>Here <code class="docutils literal notranslate"><span class="pre">constructor</span> <span class="pre">&lt;;&gt;</span> <span class="pre">numbers</span></code> is a shorthand for</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="n">constructor</span>
<span class="bp">&#183;</span> <span class="n">numbers</span>
<span class="bp">&#183;</span> <span class="n">numbers</span>
</pre></div>
</div>
<p>More generally, <code class="docutils literal notranslate"><span class="pre">&lt;;&gt;</span></code> connects two tactics, performing the second one on every goal created by the
first one.</p>
</section>
<section id="id31">
<h3><span class="section-number">4.4.5. </span>Example<a class="headerlink" href="#id31" title="Permalink to this headline">&#61633;</a></h3>
<p>Here&#8217;s a harder example, with many cases.</p>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Let <span class="math notranslate nohighlight">\(a\)</span>, <span class="math notranslate nohighlight">\(b\)</span> and <span class="math notranslate nohighlight">\(c\)</span> be positive natural numbers satisfying <span class="math notranslate nohighlight">\(a^2+b^2=c^2\)</span>.
Show that <span class="math notranslate nohighlight">\(3 \le a\)</span>.</p>
</div>
<p>Three numbers satisfying this equation are called a <em>Pythagorean triple</em>, since by Pythagoras&#8217;
theorem this means that they form the three sides of a right-angled triangle.  The natural numbers
3, 4, 5 satisfy this equation:  <span class="math notranslate nohighlight">\(3^2+4^2=5^2\)</span>.  There are other solutions, like 5, 12, 13, but
we are showing in this problem that 3, 4, 5 is the smallest solution.</p>
<div class="admonition-solution admonition">
<p class="admonition-title">Solution</p>
<p>Either <span class="math notranslate nohighlight">\(a \le 2\)</span> or  <span class="math notranslate nohighlight">\(3 \le a\)</span>.  If  <span class="math notranslate nohighlight">\(3 \le a\)</span> then we are done.  We will derive
a contradiction if  <span class="math notranslate nohighlight">\(a \le 2\)</span>.</p>
<p>Either <span class="math notranslate nohighlight">\(b \le 1\)</span> or  <span class="math notranslate nohighlight">\(2 \le b\)</span>.  We will consider these two cases separately.</p>
<p><strong>Case 1</strong> (<span class="math notranslate nohighlight">\(b \le 1\)</span>):</p>
<p>We have that</p>
<div class="math notranslate nohighlight">
\[\begin{split}c ^ 2 &amp; = a ^ 2 + b ^ 2 \\
&amp;\le 2^2+1^2\\
&amp;&lt;3^2.\end{split}\]</div>
<p>This implies that <span class="math notranslate nohighlight">\(c&lt;3\)</span>.  We now have upper bounds <span class="math notranslate nohighlight">\(a \le 2\)</span>,
<span class="math notranslate nohighlight">\(b \le 1\)</span>, <span class="math notranslate nohighlight">\(c &lt; 3\)</span>, so <span class="math notranslate nohighlight">\(a\)</span> is 1 or 2, <span class="math notranslate nohighlight">\(b\)</span> is 1, and <span class="math notranslate nohighlight">\(c\)</span> is 1 or 2.
We can analyze all these cases and check they don&#8217;t work:</p>
<div class="math notranslate nohighlight">
\[\begin{split}1^2+1^2&amp;\ne 1^2,\\
2^2+1^2&amp;\ne 1^2,\\
1^2+1^2&amp;\ne 2^2,\\
2^2+1^2&amp;\ne 2^2.\end{split}\]</div>
<p><strong>Case 2</strong> (<span class="math notranslate nohighlight">\(2 \le b\)</span>):</p>
<p>We have that</p>
<div class="math notranslate nohighlight">
\[\begin{split}b ^ 2 &amp;&lt; a ^ 2 + b ^ 2 \\
    &amp; = c ^ 2,\end{split}\]</div>
<p>so <span class="math notranslate nohighlight">\(b&lt;c\)</span>, so <span class="math notranslate nohighlight">\(b+1\le c\)</span>.  But also</p>
<div class="math notranslate nohighlight">
\[\begin{split}c ^ 2 &amp;= a ^ 2 + b ^ 2 \\
  &amp;&#8804; 2 ^ 2 + b ^ 2 \\
  &amp; = b ^ 2 + 2 \cdot 2 \\
  &amp; &#8804; b ^ 2 + 2 b \\
  &amp; &lt; b ^ 2 + 2b + 1\\
  &amp; = (b + 1) ^ 2,\end{split}\]</div>
<p>so <span class="math notranslate nohighlight">\(c&lt;b+1\)</span>, so it is false that <span class="math notranslate nohighlight">\(b+1\le c\)</span>.  These two facts contradict each other.</p>
</div>
<p>Write this proof up in Lean.  It will be long; my version is 27 lines.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">{</span><span class="n">a</span> <span class="n">b</span> <span class="n">c</span> <span class="o">:</span> <span class="n">&#8469;</span><span class="o">}</span> <span class="o">(</span><span class="n">ha</span> <span class="o">:</span> <span class="mi">0</span> <span class="bp">&lt;</span> <span class="n">a</span><span class="o">)</span> <span class="o">(</span><span class="n">hb</span> <span class="o">:</span> <span class="mi">0</span> <span class="bp">&lt;</span> <span class="n">b</span><span class="o">)</span> <span class="o">(</span><span class="n">hc</span> <span class="o">:</span> <span class="mi">0</span> <span class="bp">&lt;</span> <span class="n">c</span><span class="o">)</span>
    <span class="o">(</span><span class="n">h_pyth</span> <span class="o">:</span> <span class="n">a</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">+</span> <span class="n">b</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">=</span> <span class="n">c</span> <span class="bp">^</span> <span class="mi">2</span><span class="o">)</span> <span class="o">:</span> <span class="mi">3</span> <span class="bp">&#8804;</span> <span class="n">a</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</section>
<section id="id32">
<h3><span class="section-number">4.4.6. </span>Exercises<a class="headerlink" href="#id32" title="Permalink to this headline">&#61633;</a></h3>
<ol class="arabic">
<li><p>Let <span class="math notranslate nohighlight">\(x\)</span> and <span class="math notranslate nohighlight">\(y\)</span> be real numbers, with <span class="math notranslate nohighlight">\(x\)</span> nonnegative, and let
<span class="math notranslate nohighlight">\(n\)</span> be a positive natural number.  Prove that if <span class="math notranslate nohighlight">\(y^n \le x^n\)</span> then
<span class="math notranslate nohighlight">\(y\le x\)</span>.</p>
<p>We have used this fact before; it&#8217;s another of the lemmas which underlie the <code class="docutils literal notranslate"><span class="pre">cancel</span></code> tactic.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">{</span><span class="n">x</span> <span class="n">y</span> <span class="o">:</span> <span class="n">&#8477;</span><span class="o">}</span> <span class="o">(</span><span class="n">n</span> <span class="o">:</span> <span class="n">&#8469;</span><span class="o">)</span> <span class="o">(</span><span class="n">hx</span> <span class="o">:</span> <span class="mi">0</span> <span class="bp">&#8804;</span> <span class="n">x</span><span class="o">)</span> <span class="o">(</span><span class="n">hn</span> <span class="o">:</span> <span class="mi">0</span> <span class="bp">&lt;</span> <span class="n">n</span><span class="o">)</span> <span class="o">(</span><span class="n">h</span> <span class="o">:</span> <span class="n">y</span> <span class="bp">^</span> <span class="n">n</span> <span class="bp">&#8804;</span> <span class="n">x</span> <span class="bp">^</span> <span class="n">n</span><span class="o">)</span> <span class="o">:</span>
    <span class="n">y</span> <span class="bp">&#8804;</span> <span class="n">x</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Show that if <span class="math notranslate nohighlight">\(n^2\equiv 4\mod 5\)</span> then <span class="math notranslate nohighlight">\(n\equiv 2\mod 5\)</span> or <span class="math notranslate nohighlight">\(n\equiv 3\mod 5\)</span>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">(</span><span class="n">n</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">)</span> <span class="o">(</span><span class="n">hn</span> <span class="o">:</span> <span class="n">n</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">&#8801;</span> <span class="mi">4</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="mi">5</span><span class="o">])</span> <span class="o">:</span> <span class="n">n</span> <span class="bp">&#8801;</span> <span class="mi">2</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="mi">5</span><span class="o">]</span> <span class="bp">&#8744;</span> <span class="n">n</span> <span class="bp">&#8801;</span> <span class="mi">3</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="mi">5</span><span class="o">]</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Show that 7 is prime.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="n">Prime</span> <span class="mi">7</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Give a different proof of a problem from the exercises to <a class="reference internal" href="02_Proofs_with_Structure.html#tactic-mode"><span class="std std-numref">Section 2.1</span></a>: Let
<span class="math notranslate nohighlight">\(x\)</span>
be a rational number whose square is 4, and which is greater than 1.  Show that <span class="math notranslate nohighlight">\(x=2\)</span>.</p>
<p>Instead of using the <code class="docutils literal notranslate"><span class="pre">cancel</span></code> tactic, give a direct proof using the ideas of this section:
break into two cases, and
then rule out one of them. (You may find it convenient to deduce a numeric contradiction.)</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">{</span><span class="n">x</span> <span class="o">:</span> <span class="n">&#8474;</span><span class="o">}</span> <span class="o">(</span><span class="n">h1</span> <span class="o">:</span> <span class="n">x</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">=</span> <span class="mi">4</span><span class="o">)</span> <span class="o">(</span><span class="n">h2</span> <span class="o">:</span> <span class="mi">1</span> <span class="bp">&lt;</span> <span class="n">x</span><span class="o">)</span> <span class="o">:</span> <span class="n">x</span> <span class="bp">=</span> <span class="mi">2</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="k">have</span> <span class="n">h3</span> <span class="o">:=</span>
    <span class="k">calc</span>
      <span class="o">(</span><span class="n">x</span> <span class="bp">+</span> <span class="mi">2</span><span class="o">)</span> <span class="bp">*</span> <span class="o">(</span><span class="n">x</span> <span class="bp">-</span> <span class="mi">2</span><span class="o">)</span> <span class="bp">=</span> <span class="n">x</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">+</span> <span class="mi">2</span> <span class="bp">*</span> <span class="n">x</span> <span class="bp">-</span> <span class="mi">2</span> <span class="bp">*</span> <span class="n">x</span> <span class="bp">-</span> <span class="mi">4</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">ring</span>
      <span class="n">_</span> <span class="bp">=</span> <span class="mi">0</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">addarith</span> <span class="o">[</span><span class="n">h1</span><span class="o">]</span>
  <span class="n">rw</span> <span class="o">[</span><span class="n">mul_eq_zero</span><span class="o">]</span> <span class="n">at</span> <span class="n">h3</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Show that a prime number is either 2 or odd.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">(</span><span class="n">p</span> <span class="o">:</span> <span class="n">&#8469;</span><span class="o">)</span> <span class="o">(</span><span class="n">h</span> <span class="o">:</span> <span class="n">Prime</span> <span class="n">p</span><span class="o">)</span> <span class="o">:</span> <span class="n">p</span> <span class="bp">=</span> <span class="mi">2</span> <span class="bp">&#8744;</span> <span class="n">Odd</span> <span class="n">p</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
</ol>
</section>
</section>
<section id="proof-by-contradiction">
<span id="contradiction"></span><h2><span class="section-number">4.5. </span>Proof by contradiction<a class="headerlink" href="#proof-by-contradiction" title="Permalink to this headline">&#61633;</a></h2>
<section id="contradiction-ex1">
<span id="id33"></span><h3><span class="section-number">4.5.1. </span>Example<a class="headerlink" href="#contradiction-ex1" title="Permalink to this headline">&#61633;</a></h3>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Show that it is not true that for all real numbers <span class="math notranslate nohighlight">\(x\)</span>, we have <span class="math notranslate nohighlight">\(x^2\geq x\)</span>.</p>
</div>
<div class="admonition-solution admonition">
<p class="admonition-title">Solution</p>
<p>Suppose that for all real numbers <span class="math notranslate nohighlight">\(x\)</span>, we have <span class="math notranslate nohighlight">\(x^2\geq x\)</span>.  Then in particular
<span class="math notranslate nohighlight">\(0.5^2\geq 0.5\)</span>, but this is false, contradiction.</p>
</div>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="bp">&#172;</span> <span class="o">(</span><span class="bp">&#8704;</span> <span class="n">x</span> <span class="o">:</span> <span class="n">&#8477;</span><span class="o">,</span> <span class="n">x</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">&#8805;</span> <span class="n">x</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">intro</span> <span class="n">h</span>
  <span class="k">have</span> <span class="o">:</span> <span class="mi">0</span><span class="bp">.</span><span class="mi">5</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">&#8805;</span> <span class="mi">0</span><span class="bp">.</span><span class="mi">5</span> <span class="o">:=</span> <span class="n">h</span> <span class="mi">0</span><span class="bp">.</span><span class="mi">5</span>
  <span class="n">numbers</span> <span class="n">at</span> <span class="n">this</span>
</pre></div>
</div>
</section>
<section id="id34">
<h3><span class="section-number">4.5.2. </span>Example<a class="headerlink" href="#id34" title="Permalink to this headline">&#61633;</a></h3>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Show that 13 is not a multiple of 3.</p>
</div>
<p>In the past we have established non-divisibility facts using the theorem
<code class="docutils literal notranslate"><span class="pre">Nat.not_dvd_of_exists_lt_and_lt</span></code>.  But now we finally have the tools to do this from first
principles.</p>
<div class="admonition-solution admonition">
<p class="admonition-title">Solution</p>
<p>Suppose that 13 were a multiple of 3.  Then there would exist a natural number <span class="math notranslate nohighlight">\(k\)</span> such that
<span class="math notranslate nohighlight">\(13=3k\)</span>.</p>
<p>Case 1, <span class="math notranslate nohighlight">\(k \le 4\)</span>: Then</p>
<div class="math notranslate nohighlight">
\[\begin{split}13 &amp;= 3k \\
&amp;\le 3\cdot 4,\end{split}\]</div>
<p>contradiction.</p>
<p>Case 2, <span class="math notranslate nohighlight">\(k \ge 5\)</span>: Then</p>
<div class="math notranslate nohighlight">
\[\begin{split}13 &amp;= 3k \\
&amp;\ge 3\cdot 5,\end{split}\]</div>
<p>contradiction.</p>
</div>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="bp">&#172;</span> <span class="mi">3</span> <span class="bp">&#8739;</span> <span class="mi">13</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">intro</span> <span class="n">H</span>
  <span class="n">obtain</span> <span class="o">&#10216;</span><span class="n">k</span><span class="o">,</span> <span class="n">hk</span><span class="o">&#10217;</span> <span class="o">:=</span> <span class="n">H</span>
  <span class="n">obtain</span> <span class="n">h4</span> <span class="bp">|</span> <span class="n">h5</span> <span class="o">:=</span> <span class="n">le_or_succ_le</span> <span class="n">k</span> <span class="mi">4</span>
  <span class="bp">&#183;</span> <span class="k">have</span> <span class="n">h</span> <span class="o">:=</span>
    <span class="k">calc</span> <span class="mi">13</span> <span class="bp">=</span> <span class="mi">3</span> <span class="bp">*</span> <span class="n">k</span> <span class="o">:=</span> <span class="n">hk</span>
      <span class="n">_</span> <span class="bp">&#8804;</span> <span class="mi">3</span> <span class="bp">*</span> <span class="mi">4</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">rel</span> <span class="o">[</span><span class="n">h4</span><span class="o">]</span>
    <span class="n">numbers</span> <span class="n">at</span> <span class="n">h</span>
  <span class="bp">&#183;</span> <span class="gr">sorry</span>
</pre></div>
</div>
</section>
<section id="id35">
<h3><span class="section-number">4.5.3. </span>Example<a class="headerlink" href="#id35" title="Permalink to this headline">&#61633;</a></h3>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Let <span class="math notranslate nohighlight">\(x\)</span> and <span class="math notranslate nohighlight">\(y\)</span> be real numbers and suppose that <span class="math notranslate nohighlight">\(x+y=0\)</span>.  Show that it is not
possible for both <span class="math notranslate nohighlight">\(x\)</span> and <span class="math notranslate nohighlight">\(y\)</span> to be positive.</p>
</div>
<div class="admonition-solution admonition">
<p class="admonition-title">Solution</p>
<p>Suppose that <span class="math notranslate nohighlight">\(x\)</span> and <span class="math notranslate nohighlight">\(y\)</span> were both positive.  Then</p>
<div class="math notranslate nohighlight">
\[\begin{split}0 &amp;= x+y \\
&amp;&gt; 0,\end{split}\]</div>
<p>contradiction.</p>
</div>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">{</span><span class="n">x</span> <span class="n">y</span> <span class="o">:</span> <span class="n">&#8477;</span><span class="o">}</span> <span class="o">(</span><span class="n">h</span> <span class="o">:</span> <span class="n">x</span> <span class="bp">+</span> <span class="n">y</span> <span class="bp">=</span> <span class="mi">0</span><span class="o">)</span> <span class="o">:</span> <span class="bp">&#172;</span><span class="o">(</span><span class="n">x</span> <span class="bp">&gt;</span> <span class="mi">0</span> <span class="bp">&#8743;</span> <span class="n">y</span> <span class="bp">&gt;</span> <span class="mi">0</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">intro</span> <span class="n">h</span>
  <span class="n">obtain</span> <span class="o">&#10216;</span><span class="n">hx</span><span class="o">,</span> <span class="n">hy</span><span class="o">&#10217;</span> <span class="o">:=</span> <span class="n">h</span>
  <span class="k">have</span> <span class="n">H</span> <span class="o">:=</span>
  <span class="k">calc</span> <span class="mi">0</span> <span class="bp">=</span> <span class="n">x</span> <span class="bp">+</span> <span class="n">y</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">rw</span> <span class="o">[</span><span class="n">h</span><span class="o">]</span>
    <span class="n">_</span> <span class="bp">&gt;</span> <span class="mi">0</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">extra</span>
  <span class="n">numbers</span> <span class="n">at</span> <span class="n">H</span>
</pre></div>
</div>
</section>
<section id="sq-ne-two">
<span id="id36"></span><h3><span class="section-number">4.5.4. </span>Example<a class="headerlink" href="#sq-ne-two" title="Permalink to this headline">&#61633;</a></h3>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Show that there does not exist a natural number <span class="math notranslate nohighlight">\(n\)</span>, such that <span class="math notranslate nohighlight">\(n^2=2\)</span>.</p>
</div>
<p>(Compare this with <a class="reference internal" href="02_Proofs_with_Structure.html#sq-ne-two"><span class="std std-numref">Example 2.3.2</span></a>.)</p>
<div class="admonition-solution admonition">
<p class="admonition-title">Solution</p>
<p>Suppose that some integer <span class="math notranslate nohighlight">\(n\)</span> satisfied <span class="math notranslate nohighlight">\(n^2=2\)</span>.</p>
<p>Case 1, <span class="math notranslate nohighlight">\(n \le 1\)</span>: Then</p>
<div class="math notranslate nohighlight">
\[\begin{split}2 &amp;= n^2 \\
&amp;\le 1^2,\end{split}\]</div>
<p>contradiction.</p>
<p>Case 2, <span class="math notranslate nohighlight">\(n \ge 2\)</span>: Then</p>
<div class="math notranslate nohighlight">
\[\begin{split}2 &amp;= n^2 \\
&amp;\ge 2^2,\end{split}\]</div>
<p>contradiction.</p>
</div>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="bp">&#172;</span> <span class="o">(</span><span class="bp">&#8707;</span> <span class="n">n</span> <span class="o">:</span> <span class="n">&#8469;</span><span class="o">,</span> <span class="n">n</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">=</span> <span class="mi">2</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</section>
<section id="even-iff-not-odd">
<span id="id37"></span><h3><span class="section-number">4.5.5. </span>Example<a class="headerlink" href="#even-iff-not-odd" title="Permalink to this headline">&#61633;</a></h3>
<div class="admonition-lemma admonition">
<p class="admonition-title">Lemma</p>
<p>Show that an integer <span class="math notranslate nohighlight">\(n\)</span> is even if and only if it is not odd.</p>
</div>
<div class="admonition-proof admonition">
<p class="admonition-title">Proof</p>
<p>First, let <span class="math notranslate nohighlight">\(n\)</span> be even, and suppose that it were also odd.  Then <span class="math notranslate nohighlight">\(n\equiv 0\mod 2\)</span>
but also <span class="math notranslate nohighlight">\(n\equiv 1\mod 2\)</span>.  So</p>
<div class="math notranslate nohighlight">
\[\begin{split}0 &amp;\equiv n \mod 2 \\
&amp;\equiv 1\mod 2,\end{split}\]</div>
<p>contradiction.</p>
<p>Now, suppose that <span class="math notranslate nohighlight">\(n\)</span> is not odd.  Since <span class="math notranslate nohighlight">\(n\)</span> has to be either even or odd, it is even.</p>
</div>
<p>We record this for future use in Lean problems under the name <code class="docutils literal notranslate"><span class="pre">Int.even_iff_not_odd</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">(</span><span class="n">n</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">)</span> <span class="o">:</span> <span class="n">Int.Even</span> <span class="n">n</span> <span class="bp">&#8596;</span> <span class="bp">&#172;</span> <span class="n">Int.Odd</span> <span class="n">n</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">constructor</span>
  <span class="bp">&#183;</span> <span class="n">intro</span> <span class="n">h1</span> <span class="n">h2</span>
    <span class="n">rw</span> <span class="o">[</span><span class="n">Int.even_iff_modEq</span><span class="o">]</span> <span class="n">at</span> <span class="n">h1</span>
    <span class="n">rw</span> <span class="o">[</span><span class="n">Int.odd_iff_modEq</span><span class="o">]</span> <span class="n">at</span> <span class="n">h2</span>
    <span class="k">have</span> <span class="n">h</span> <span class="o">:=</span>
    <span class="k">calc</span> <span class="mi">0</span> <span class="bp">&#8801;</span> <span class="n">n</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="mi">2</span><span class="o">]</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">rel</span> <span class="o">[</span><span class="n">h1</span><span class="o">]</span>
      <span class="n">_</span> <span class="bp">&#8801;</span> <span class="mi">1</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="mi">2</span><span class="o">]</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">rel</span> <span class="o">[</span><span class="n">h2</span><span class="o">]</span>
    <span class="n">numbers</span> <span class="n">at</span> <span class="n">h</span> <span class="c1">-- contradiction!</span>
  <span class="bp">&#183;</span> <span class="n">intro</span> <span class="n">h</span>
    <span class="n">obtain</span> <span class="n">h1</span> <span class="bp">|</span> <span class="n">h2</span> <span class="o">:=</span> <span class="n">Int.even_or_odd</span> <span class="n">n</span>
    <span class="bp">&#183;</span> <span class="n">apply</span> <span class="n">h1</span>
    <span class="bp">&#183;</span> <span class="n">contradiction</span>
</pre></div>
</div>
<p>Now repeat the process to characterise &#8220;not-even.&#8221;</p>
<div class="admonition-lemma admonition">
<p class="admonition-title">Lemma</p>
<p>Show that an integer <span class="math notranslate nohighlight">\(n\)</span> is odd if and only if it is not even.</p>
</div>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">(</span><span class="n">n</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">)</span> <span class="o">:</span> <span class="n">Int.Odd</span> <span class="n">n</span> <span class="bp">&#8596;</span> <span class="bp">&#172;</span> <span class="n">Int.Even</span> <span class="n">n</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</section>
<section id="id38">
<h3><span class="section-number">4.5.6. </span>Example<a class="headerlink" href="#id38" title="Permalink to this headline">&#61633;</a></h3>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Let <span class="math notranslate nohighlight">\(n\)</span> be an integer.  Show that <span class="math notranslate nohighlight">\(n^2\not\equiv 2 \mod 3\)</span>.</p>
</div>
<div class="admonition-solution admonition">
<p class="admonition-title">Solution</p>
<p>Suppose that  <span class="math notranslate nohighlight">\(n^2\equiv 2 \mod 3\)</span>.
We consider cases according to the residue of <span class="math notranslate nohighlight">\(n\)</span> modulo 3.</p>
<p>If <span class="math notranslate nohighlight">\(n\equiv 0 \mod 3\)</span>, then</p>
<div class="math notranslate nohighlight">
\[\begin{split}0 &amp;= 0^2 \\
&amp;\equiv n^2 \mod 3 \\
&amp;\equiv 2 \mod 3,\end{split}\]</div>
<p>contradiction.</p>
<p>If <span class="math notranslate nohighlight">\(n\equiv 1 \mod 3\)</span>, then</p>
<div class="math notranslate nohighlight">
\[\begin{split}1 &amp;= 1^2 \\
&amp;\equiv n^2 \mod 3 \\
&amp;\equiv 2 \mod 3,\end{split}\]</div>
<p>contradiction.</p>
<p>Finally, if <span class="math notranslate nohighlight">\(n\equiv 2 \mod 3\)</span>, then</p>
<div class="math notranslate nohighlight">
\[\begin{split}1 &amp;\equiv 1 + 3 \cdot 1\mod 3\\
&amp;=2^2 \\
&amp;\equiv n^2 \mod 3 \\
&amp;\equiv 2 \mod 3,\end{split}\]</div>
<p>contradiction.</p>
</div>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">(</span><span class="n">n</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">)</span> <span class="o">:</span> <span class="bp">&#172;</span><span class="o">(</span><span class="n">n</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">&#8801;</span> <span class="mi">2</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="mi">3</span><span class="o">])</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">intro</span> <span class="n">h</span>
  <span class="n">mod_cases</span> <span class="n">hn</span> <span class="o">:</span> <span class="n">n</span> <span class="bp">%</span> <span class="mi">3</span>
  <span class="bp">&#183;</span> <span class="k">have</span> <span class="n">h</span> <span class="o">:=</span>
    <span class="k">calc</span> <span class="o">(</span><span class="mi">0</span><span class="o">:</span><span class="n">&#8484;</span><span class="o">)</span> <span class="bp">=</span> <span class="mi">0</span> <span class="bp">^</span> <span class="mi">2</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">numbers</span>
      <span class="n">_</span> <span class="bp">&#8801;</span> <span class="n">n</span> <span class="bp">^</span> <span class="mi">2</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="mi">3</span><span class="o">]</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">rel</span> <span class="o">[</span><span class="n">hn</span><span class="o">]</span>
      <span class="n">_</span> <span class="bp">&#8801;</span> <span class="mi">2</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="mi">3</span><span class="o">]</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">rel</span> <span class="o">[</span><span class="n">h</span><span class="o">]</span>
    <span class="n">numbers</span> <span class="n">at</span> <span class="n">h</span> <span class="c1">-- contradiction!</span>
  <span class="bp">&#183;</span> <span class="gr">sorry</span>
  <span class="bp">&#183;</span> <span class="gr">sorry</span>
</pre></div>
</div>
</section>
<section id="not-prime-proof">
<span id="id39"></span><h3><span class="section-number">4.5.7. </span>Example<a class="headerlink" href="#not-prime-proof" title="Permalink to this headline">&#61633;</a></h3>
<p>We can now pay a couple of debts.  First, there is this theorem, first mentioned in
<a class="reference internal" href="#not-prime"><span class="std std-numref">Example 4.1.9</span></a>:</p>
<div class="admonition-theorem admonition">
<p class="admonition-title">Theorem</p>
<p>Let <span class="math notranslate nohighlight">\(p\)</span>, <span class="math notranslate nohighlight">\(k\)</span> and <span class="math notranslate nohighlight">\(l\)</span> be natural numbers, with <span class="math notranslate nohighlight">\(k\ne 1\)</span>, <span class="math notranslate nohighlight">\(k\ne p\)</span>, and
<span class="math notranslate nohighlight">\(p=kl\)</span>.  Then <span class="math notranslate nohighlight">\(p\)</span> is not prime.</p>
</div>
<div class="admonition-proof admonition">
<p class="admonition-title">Proof</p>
<p><span class="math notranslate nohighlight">\(k\)</span> is a factor of <span class="math notranslate nohighlight">\(p\)</span>.  If <span class="math notranslate nohighlight">\(p\)</span> were prime, then by definition for any factor
<span class="math notranslate nohighlight">\(x\)</span> of <span class="math notranslate nohighlight">\(p\)</span> either
<span class="math notranslate nohighlight">\(x=1\)</span> or <span class="math notranslate nohighlight">\(x=p\)</span>, so in particular <span class="math notranslate nohighlight">\(k=1\)</span> or <span class="math notranslate nohighlight">\(k=p\)</span>. But either of these
contradicts a hypothesis.</p>
</div>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">{</span><span class="n">p</span> <span class="o">:</span> <span class="n">&#8469;</span><span class="o">}</span> <span class="o">(</span><span class="n">k</span> <span class="n">l</span> <span class="o">:</span> <span class="n">&#8469;</span><span class="o">)</span> <span class="o">(</span><span class="n">hk1</span> <span class="o">:</span> <span class="n">k</span> <span class="bp">&#8800;</span> <span class="mi">1</span><span class="o">)</span> <span class="o">(</span><span class="n">hkp</span> <span class="o">:</span> <span class="n">k</span> <span class="bp">&#8800;</span> <span class="n">p</span><span class="o">)</span> <span class="o">(</span><span class="n">hkl</span> <span class="o">:</span> <span class="n">p</span> <span class="bp">=</span> <span class="n">k</span> <span class="bp">*</span> <span class="n">l</span><span class="o">)</span> <span class="o">:</span>
    <span class="bp">&#172;</span><span class="o">(</span><span class="n">Prime</span> <span class="n">p</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="k">have</span> <span class="n">hk</span> <span class="o">:</span> <span class="n">k</span> <span class="bp">&#8739;</span> <span class="n">p</span>
  <span class="bp">&#183;</span> <span class="n">use</span> <span class="n">l</span>
    <span class="n">apply</span> <span class="n">hkl</span>
  <span class="n">intro</span> <span class="n">h</span>
  <span class="n">obtain</span> <span class="o">&#10216;</span><span class="n">h2</span><span class="o">,</span> <span class="n">hfact</span><span class="o">&#10217;</span> <span class="o">:=</span> <span class="n">h</span>
  <span class="k">have</span> <span class="o">:</span> <span class="n">k</span> <span class="bp">=</span> <span class="mi">1</span> <span class="bp">&#8744;</span> <span class="n">k</span> <span class="bp">=</span> <span class="n">p</span> <span class="o">:=</span> <span class="n">hfact</span> <span class="n">k</span> <span class="n">hk</span>
  <span class="n">obtain</span> <span class="n">hk1&#39;</span> <span class="bp">|</span> <span class="n">hkp&#39;</span> <span class="o">:=</span> <span class="n">this</span>
  <span class="bp">&#183;</span> <span class="n">contradiction</span>
  <span class="bp">&#183;</span> <span class="n">contradiction</span>
</pre></div>
</div>
</section>
<section id="not-divisible-proof">
<span id="id40"></span><h3><span class="section-number">4.5.8. </span>Example<a class="headerlink" href="#not-divisible-proof" title="Permalink to this headline">&#61633;</a></h3>
<p>Secondly, there is this theorem, first mentioned in <a class="reference internal" href="03_Parity_and_Divisibility.html#not-divisible"><span class="std std-numref">Example 3.2.6</span></a>:</p>
<div class="admonition-theorem admonition">
<p class="admonition-title">Theorem</p>
<p>Let <span class="math notranslate nohighlight">\(a\)</span> and <span class="math notranslate nohighlight">\(b\)</span> be integers.  If there exists an
integer <span class="math notranslate nohighlight">\(q\)</span> such that <span class="math notranslate nohighlight">\(bq&lt;a&lt;b(q + 1)\)</span>, then <span class="math notranslate nohighlight">\(a\)</span> is not a multiple
of <span class="math notranslate nohighlight">\(b\)</span>.</p>
</div>
<p>This is the lemma we have invoked in Lean as <code class="docutils literal notranslate"><span class="pre">Int.not_dvd_of_exists_lt_and_lt</span></code>.</p>
<div class="admonition-proof admonition">
<p class="admonition-title">Proof</p>
<p>Suppose for the sake of contradiction that <span class="math notranslate nohighlight">\(a\)</span> is a multiple of <span class="math notranslate nohighlight">\(b\)</span>. Then there exists
an integer <span class="math notranslate nohighlight">\(k\)</span> such that <span class="math notranslate nohighlight">\(a=bk\)</span>.  Also, let <span class="math notranslate nohighlight">\(q\)</span> be an integer such that
<span class="math notranslate nohighlight">\(b q&lt;a&lt;b(q + 1)\)</span>.</p>
<p>We first note that</p>
<div class="math notranslate nohighlight">
\[\begin{split}0 &amp;= a - a\\
&amp;&lt; b(q+1)-bq\\
&amp;=b.\end{split}\]</div>
<p>Now let us reason from the two known inequalities separately. We first observe that</p>
<div class="math notranslate nohighlight">
\[\begin{split}bk &amp;=a \\
  &amp; &lt; b(q+1),\end{split}\]</div>
<p>and so (since <span class="math notranslate nohighlight">\(b&gt;0\)</span>) we have <span class="math notranslate nohighlight">\(k &lt; q+1\)</span>.</p>
<p>We next observe that</p>
<div class="math notranslate nohighlight">
\[\begin{split}bq &amp;&lt; a \\
  &amp; =bk,\end{split}\]</div>
<p>and so  (since <span class="math notranslate nohighlight">\(b&gt;0\)</span>) we have <span class="math notranslate nohighlight">\(q &lt; k\)</span>, thus <span class="math notranslate nohighlight">\(q+1 \le k\)</span>.</p>
<p>These two facts contradict each other, so <span class="math notranslate nohighlight">\(a\)</span> must not be a multiple of <span class="math notranslate nohighlight">\(b\)</span> after all.</p>
</div>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">(</span><span class="n">a</span> <span class="n">b</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">)</span> <span class="o">(</span><span class="n">h</span> <span class="o">:</span> <span class="bp">&#8707;</span> <span class="n">q</span><span class="o">,</span> <span class="n">b</span> <span class="bp">*</span> <span class="n">q</span> <span class="bp">&lt;</span> <span class="n">a</span> <span class="bp">&#8743;</span> <span class="n">a</span> <span class="bp">&lt;</span> <span class="n">b</span> <span class="bp">*</span> <span class="o">(</span><span class="n">q</span> <span class="bp">+</span> <span class="mi">1</span><span class="o">))</span> <span class="o">:</span> <span class="bp">&#172;</span><span class="n">b</span> <span class="bp">&#8739;</span> <span class="n">a</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">intro</span> <span class="n">H</span>
  <span class="n">obtain</span> <span class="o">&#10216;</span><span class="n">k</span><span class="o">,</span> <span class="n">hk</span><span class="o">&#10217;</span> <span class="o">:=</span> <span class="n">H</span>
  <span class="n">obtain</span> <span class="o">&#10216;</span><span class="n">q</span><span class="o">,</span> <span class="n">hq&#8321;</span><span class="o">,</span> <span class="n">hq&#8322;</span><span class="o">&#10217;</span> <span class="o">:=</span> <span class="n">h</span>
  <span class="k">have</span> <span class="n">hb</span> <span class="o">:=</span>
  <span class="k">calc</span> <span class="mi">0</span> <span class="bp">=</span> <span class="n">a</span> <span class="bp">-</span> <span class="n">a</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">ring</span>
    <span class="n">_</span> <span class="bp">&lt;</span> <span class="n">b</span> <span class="bp">*</span> <span class="o">(</span><span class="n">q</span> <span class="bp">+</span> <span class="mi">1</span><span class="o">)</span> <span class="bp">-</span> <span class="n">b</span> <span class="bp">*</span> <span class="n">q</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">rel</span> <span class="o">[</span><span class="n">hq&#8321;</span><span class="o">,</span> <span class="n">hq&#8322;</span><span class="o">]</span>
    <span class="n">_</span> <span class="bp">=</span> <span class="n">b</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">ring</span>
  <span class="k">have</span> <span class="n">h1</span> <span class="o">:=</span>
  <span class="k">calc</span> <span class="n">b</span> <span class="bp">*</span> <span class="n">k</span> <span class="bp">=</span> <span class="n">a</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">rw</span> <span class="o">[</span><span class="n">hk</span><span class="o">]</span>
    <span class="n">_</span> <span class="bp">&lt;</span> <span class="n">b</span> <span class="bp">*</span> <span class="o">(</span><span class="n">q</span> <span class="bp">+</span> <span class="mi">1</span><span class="o">)</span> <span class="o">:=</span> <span class="n">hq&#8322;</span>
  <span class="n">cancel</span> <span class="n">b</span> <span class="n">at</span> <span class="n">h1</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</section>
<section id="better-prime-test">
<span id="id41"></span><h3><span class="section-number">4.5.9. </span>Example<a class="headerlink" href="#better-prime-test" title="Permalink to this headline">&#61633;</a></h3>
<p>We also establish a test for primality which will be more efficient than the test from
<a class="reference internal" href="#prime-test"><span class="std std-numref">Example 4.4.4</span></a>.</p>
<div class="admonition-theorem admonition">
<p class="admonition-title">Theorem</p>
<p>Let <span class="math notranslate nohighlight">\(p\)</span> be a natural number which is at least 2. Let <span class="math notranslate nohighlight">\(T\)</span> be another natural number,
whose square is greater than <span class="math notranslate nohighlight">\(p\)</span>, and suppose that every natural number <span class="math notranslate nohighlight">\(m\)</span>
for which <span class="math notranslate nohighlight">\(1&lt;m&lt;T\)</span> is not a factor of <span class="math notranslate nohighlight">\(p\)</span>.  Then <span class="math notranslate nohighlight">\(p\)</span> is prime.</p>
</div>
<p>(Notice that in the <a class="reference internal" href="#prime-test"><span class="std std-numref">Example 4.4.4</span></a> test we had to check that every number up to
<span class="math notranslate nohighlight">\(p\)</span> was not a factor of <span class="math notranslate nohighlight">\(p\)</span>; with this test we only need to check the numbers up to
approximately the square root of <span class="math notranslate nohighlight">\(p\)</span>.)</p>
<div class="admonition-proof admonition">
<p class="admonition-title">Proof</p>
<p>By the prime test from <a class="reference internal" href="#prime-test"><span class="std std-numref">Example 4.4.4</span></a>, it suffices to show that every natural
number <span class="math notranslate nohighlight">\(m\)</span> with <span class="math notranslate nohighlight">\(1&lt;m&lt;p\)</span> is not a factor of <span class="math notranslate nohighlight">\(p\)</span>.  Let <span class="math notranslate nohighlight">\(m\)</span> be such a natural
number.  If <span class="math notranslate nohighlight">\(m &lt; T\)</span> then by hypothesis <span class="math notranslate nohighlight">\(m\)</span> is not a factor of <span class="math notranslate nohighlight">\(p\)</span>.</p>
<p>So suppose that <span class="math notranslate nohighlight">\(T \le  m\)</span>, and that <span class="math notranslate nohighlight">\(m\)</span> is a factor of <span class="math notranslate nohighlight">\(p\)</span>.  Then there exists a
natural number <span class="math notranslate nohighlight">\(l\)</span> such that <span class="math notranslate nohighlight">\(p= ml\)</span>.  The natural number <span class="math notranslate nohighlight">\(l\)</span> is a factor of
<span class="math notranslate nohighlight">\(p\)</span>, too.</p>
<p>We claim that <span class="math notranslate nohighlight">\(1&lt;l\)</span>.  It will suffice to show that <span class="math notranslate nohighlight">\(m \cdot 1 &lt; ml\)</span>, and indeed,</p>
<div class="math notranslate nohighlight">
\[\begin{split}m\cdot 1 &amp;=m \\
  &amp; &lt; p\\
  &amp;=ml.\end{split}\]</div>
<p>We also claim that <span class="math notranslate nohighlight">\(l&lt;T\)</span>.  It will suffice to show that <span class="math notranslate nohighlight">\(Tl &lt; T \cdot T\)</span>, and indeed,</p>
<div class="math notranslate nohighlight">
\[\begin{split}Tl &amp; \le ml \\
  &amp; =p\\
  &amp;&lt; T^2\\
  &amp;=T\cdot T.\end{split}\]</div>
<p>Since we have established that <span class="math notranslate nohighlight">\(1&lt;l&lt;T\)</span>, by hypothesis <span class="math notranslate nohighlight">\(l\)</span> is not a factor of
<span class="math notranslate nohighlight">\(p\)</span>, contradiction.  So <span class="math notranslate nohighlight">\(m\)</span> must not be a factor of <span class="math notranslate nohighlight">\(p\)</span> after all.</p>
</div>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">{</span><span class="n">p</span> <span class="o">:</span> <span class="n">&#8469;</span><span class="o">}</span> <span class="o">(</span><span class="n">hp</span> <span class="o">:</span> <span class="mi">2</span> <span class="bp">&#8804;</span> <span class="n">p</span><span class="o">)</span>  <span class="o">(</span><span class="n">T</span> <span class="o">:</span> <span class="n">&#8469;</span><span class="o">)</span> <span class="o">(</span><span class="n">hTp</span> <span class="o">:</span> <span class="n">p</span> <span class="bp">&lt;</span> <span class="n">T</span> <span class="bp">^</span> <span class="mi">2</span><span class="o">)</span>
    <span class="o">(</span><span class="n">H</span> <span class="o">:</span> <span class="bp">&#8704;</span> <span class="o">(</span><span class="n">m</span> <span class="o">:</span> <span class="n">&#8469;</span><span class="o">),</span> <span class="mi">1</span> <span class="bp">&lt;</span> <span class="n">m</span> <span class="bp">&#8594;</span> <span class="n">m</span> <span class="bp">&lt;</span> <span class="n">T</span> <span class="bp">&#8594;</span> <span class="bp">&#172;</span> <span class="o">(</span><span class="n">m</span> <span class="bp">&#8739;</span> <span class="n">p</span><span class="o">))</span> <span class="o">:</span>
    <span class="n">Prime</span> <span class="n">p</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">apply</span> <span class="n">prime_test</span> <span class="n">hp</span>
  <span class="n">intro</span> <span class="n">m</span> <span class="n">hm1</span> <span class="n">hmp</span>
  <span class="n">obtain</span> <span class="n">hmT</span> <span class="bp">|</span> <span class="n">hmT</span> <span class="o">:=</span> <span class="n">lt_or_le</span> <span class="n">m</span> <span class="n">T</span>
  <span class="bp">&#183;</span> <span class="n">apply</span> <span class="n">H</span> <span class="n">m</span> <span class="n">hm1</span> <span class="n">hmT</span>
  <span class="n">intro</span> <span class="n">h_div</span>
  <span class="n">obtain</span> <span class="o">&#10216;</span><span class="n">l</span><span class="o">,</span> <span class="n">hl</span><span class="o">&#10217;</span> <span class="o">:=</span> <span class="n">h_div</span>
  <span class="k">have</span> <span class="o">:</span> <span class="n">l</span> <span class="bp">&#8739;</span> <span class="n">p</span>
  <span class="bp">&#183;</span> <span class="gr">sorry</span>
  <span class="k">have</span> <span class="n">hl1</span> <span class="o">:=</span>
    <span class="k">calc</span> <span class="n">m</span> <span class="bp">*</span> <span class="mi">1</span> <span class="bp">=</span> <span class="n">m</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">ring</span>
      <span class="n">_</span> <span class="bp">&lt;</span> <span class="n">p</span> <span class="o">:=</span> <span class="n">hmp</span>
      <span class="n">_</span> <span class="bp">=</span> <span class="n">m</span> <span class="bp">*</span> <span class="n">l</span> <span class="o">:=</span> <span class="n">hl</span>
  <span class="n">cancel</span> <span class="n">m</span> <span class="n">at</span> <span class="n">hl1</span>
  <span class="k">have</span> <span class="n">hl2</span> <span class="o">:</span> <span class="n">l</span> <span class="bp">&lt;</span> <span class="n">T</span>
  <span class="bp">&#183;</span> <span class="gr">sorry</span>
  <span class="k">have</span> <span class="o">:</span> <span class="bp">&#172;</span> <span class="n">l</span> <span class="bp">&#8739;</span> <span class="n">p</span> <span class="o">:=</span> <span class="n">H</span> <span class="n">l</span> <span class="n">hl1</span> <span class="n">hl2</span>
  <span class="n">contradiction</span>
</pre></div>
</div>
<p>We record this for future use under the Lean name <code class="docutils literal notranslate"><span class="pre">better_prime_test</span></code>.</p>
<p>Here&#8217;s an example of how this prime-testing lemma is used.  I have left some of the later cases
for you to check.</p>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Show that 79 is prime.</p>
</div>
<div class="admonition-solution admonition">
<p class="admonition-title">Solution</p>
<p>Clearly <span class="math notranslate nohighlight">\(2 &#8804; 79\)</span>.  Also notice that <span class="math notranslate nohighlight">\(79&lt;9^2\)</span>. Let <span class="math notranslate nohighlight">\(m\)</span> be a natural number with
<span class="math notranslate nohighlight">\(1&lt;m&lt;9\)</span>.  We will show that 79 is not a multiple of <span class="math notranslate nohighlight">\(m\)</span>. There are seven cases to
check:</p>
<p><strong>Case 1</strong> (<span class="math notranslate nohighlight">\(m=2\)</span>):  Since 79 lies between the consecutive multiples
<span class="math notranslate nohighlight">\(2\cdot 39\)</span> and <span class="math notranslate nohighlight">\(2 \cdot 40\)</span> of 2, it is not a multiple of 2.</p>
<p><strong>Case 2</strong> (<span class="math notranslate nohighlight">\(m=3\)</span>):  Since 79 lies between the consecutive multiples
<span class="math notranslate nohighlight">\(3\cdot 26\)</span> and <span class="math notranslate nohighlight">\(3 \cdot 27\)</span> of 3, it is not a multiple of 3.</p>
<p><strong>Case 3</strong> (<span class="math notranslate nohighlight">\(m=4\)</span>):  Since 79 lies between the consecutive multiples
<span class="math notranslate nohighlight">\(4\cdot 19\)</span> and <span class="math notranslate nohighlight">\(4 \cdot 20\)</span> of 4, it is not a multiple of 4.</p>
<p>(etc. for 5, 6, 7 and 8)</p>
</div>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="n">Prime</span> <span class="mi">79</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">apply</span> <span class="n">better_prime_test</span> <span class="o">(</span><span class="n">T</span> <span class="o">:=</span> <span class="mi">9</span><span class="o">)</span>
  <span class="bp">&#183;</span> <span class="n">numbers</span>
  <span class="bp">&#183;</span> <span class="n">numbers</span>
  <span class="n">intro</span> <span class="n">m</span> <span class="n">hm1</span> <span class="n">hm2</span>
  <span class="n">apply</span> <span class="n">Nat.not_dvd_of_exists_lt_and_lt</span>
  <span class="n">interval_cases</span> <span class="n">m</span>
  <span class="bp">&#183;</span> <span class="n">use</span> <span class="mi">39</span>
    <span class="n">constructor</span> <span class="bp">&lt;;&gt;</span> <span class="n">numbers</span>
  <span class="bp">&#183;</span> <span class="n">use</span> <span class="mi">26</span>
    <span class="n">constructor</span> <span class="bp">&lt;;&gt;</span> <span class="n">numbers</span>
  <span class="bp">&#183;</span> <span class="n">use</span> <span class="mi">19</span>
    <span class="n">constructor</span> <span class="bp">&lt;;&gt;</span> <span class="n">numbers</span>
  <span class="bp">&#183;</span> <span class="gr">sorry</span>
  <span class="bp">&#183;</span> <span class="gr">sorry</span>
  <span class="bp">&#183;</span> <span class="gr">sorry</span>
  <span class="bp">&#183;</span> <span class="gr">sorry</span>
</pre></div>
</div>
</section>
<section id="id42">
<h3><span class="section-number">4.5.10. </span>Exercises<a class="headerlink" href="#id42" title="Permalink to this headline">&#61633;</a></h3>
<ol class="arabic">
<li><p>Show that there does not exist a real number <span class="math notranslate nohighlight">\(t\)</span>, such that <span class="math notranslate nohighlight">\(t \le 4\)</span> and
<span class="math notranslate nohighlight">\(t\geq 5\)</span>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="bp">&#172;</span> <span class="o">(</span><span class="bp">&#8707;</span> <span class="n">t</span> <span class="o">:</span> <span class="n">&#8477;</span><span class="o">,</span> <span class="n">t</span> <span class="bp">&#8804;</span> <span class="mi">4</span> <span class="bp">&#8743;</span> <span class="n">t</span> <span class="bp">&#8805;</span> <span class="mi">5</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Show that there does not exist a real number <span class="math notranslate nohighlight">\(a\)</span>, such that <span class="math notranslate nohighlight">\(a^2 \le 8\)</span> and
<span class="math notranslate nohighlight">\(a^3\geq 30\)</span>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="bp">&#172;</span> <span class="o">(</span><span class="bp">&#8707;</span> <span class="n">a</span> <span class="o">:</span> <span class="n">&#8477;</span><span class="o">,</span> <span class="n">a</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">&#8804;</span> <span class="mi">8</span> <span class="bp">&#8743;</span> <span class="n">a</span> <span class="bp">^</span> <span class="mi">3</span> <span class="bp">&#8805;</span> <span class="mi">30</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Show that 7 is not even.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="bp">&#172;</span> <span class="n">Int.Even</span> <span class="mi">7</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Let <span class="math notranslate nohighlight">\(n\)</span> be an integer satisfying <span class="math notranslate nohighlight">\(n+3=7\)</span>.  Show that <span class="math notranslate nohighlight">\(n\)</span> cannot be both
even and a solution to <span class="math notranslate nohighlight">\(n^2=10\)</span>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">{</span><span class="n">n</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">}</span> <span class="o">(</span><span class="n">hn</span> <span class="o">:</span> <span class="n">n</span> <span class="bp">+</span> <span class="mi">3</span> <span class="bp">=</span> <span class="mi">7</span><span class="o">)</span> <span class="o">:</span> <span class="bp">&#172;</span> <span class="o">(</span><span class="n">Int.Even</span> <span class="n">n</span> <span class="bp">&#8743;</span> <span class="n">n</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">=</span> <span class="mi">10</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Let <span class="math notranslate nohighlight">\(x\)</span> be a real number satisfying <span class="math notranslate nohighlight">\(x^2&lt;9\)</span>.  Show that <span class="math notranslate nohighlight">\(x\)</span> cannot be either
less than or equal to -3, or greater than or equal to 3.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">{</span><span class="n">x</span> <span class="o">:</span> <span class="n">&#8477;</span><span class="o">}</span> <span class="o">(</span><span class="n">hx</span> <span class="o">:</span> <span class="n">x</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">&lt;</span> <span class="mi">9</span><span class="o">)</span> <span class="o">:</span> <span class="bp">&#172;</span> <span class="o">(</span><span class="n">x</span> <span class="bp">&#8804;</span> <span class="bp">-</span><span class="mi">3</span> <span class="bp">&#8744;</span> <span class="n">x</span> <span class="bp">&#8805;</span> <span class="mi">3</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Show that there does not exist a natural number <span class="math notranslate nohighlight">\(N\)</span>, such that every natural number
greater than <span class="math notranslate nohighlight">\(N\)</span> is even.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="bp">&#172;</span> <span class="o">(</span><span class="bp">&#8707;</span> <span class="n">N</span> <span class="o">:</span> <span class="n">&#8469;</span><span class="o">,</span> <span class="bp">&#8704;</span> <span class="n">k</span> <span class="bp">&gt;</span> <span class="n">N</span><span class="o">,</span> <span class="n">Nat.Even</span> <span class="n">k</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Let <span class="math notranslate nohighlight">\(n\)</span> be an integer.  Show that <span class="math notranslate nohighlight">\(n^2\not\equiv 2 \mod 4\)</span>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">(</span><span class="n">n</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">)</span> <span class="o">:</span> <span class="bp">&#172;</span><span class="o">(</span><span class="n">n</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">&#8801;</span> <span class="mi">2</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="mi">4</span><span class="o">])</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Show that 1 is not prime.</p>
<p>We record this lemma for future use under the name <code class="docutils literal notranslate"><span class="pre">not_prime_one</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="bp">&#172;</span> <span class="n">Prime</span> <span class="mi">1</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Show that 97 is prime.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="n">Prime</span> <span class="mi">97</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
</ol>
</section>
</section>
</section>


           </div>
          </div>
          <footer><div class="rst-footer-buttons" role="navigation" aria-label="Footer">
        <a href="03_Parity_and_Divisibility.html" class="btn btn-neutral float-left" title="3. Parity and divisibility" accesskey="p" rel="prev"><span class="fa fa-arrow-circle-left" aria-hidden="true"></span> Previous</a>
        <a href="05_Logic.html" class="btn btn-neutral float-right" title="5. Logic" accesskey="n" rel="next">Next <span class="fa fa-arrow-circle-right" aria-hidden="true"></span></a>
    </div>

  <hr/>

  <div role="contentinfo">
    <p>&#169; Copyright 2022-2024, Heather Macbeth.  All rights reserved.</p>
  </div>

  Built with <a href="https://www.sphinx-doc.org/">Sphinx</a> using a
    <a href="https://github.com/readthedocs/sphinx_rtd_theme">theme</a>
    provided by <a href="https://readthedocs.org">Read the Docs</a>.
   

</footer>
        </div>
      </div>
    </section>
  </div>
  <script>
      jQuery(function () {
          SphinxRtdTheme.Navigation.enable(true);
      });
  </script> 

</body>
</html>